Cardanoにおけるスマートコントラクト検証の新時代

Cardanoでは、スマートコントラクトはPlinth、Aiken、Plu–tsなどの強力な表層言語で作成される。これらのコントラクトは現実の貴重な資産をコントロールする。失敗した場合、資金は盗まれたり永久にロックされたりする可能性がある。

Input | Output (IO)は、Cardanoスマートコントラクトに形式検証をもたらす新しいツールを開発している。AGDA、ROQ（旧Coq）、その他の証明支援系のようなシステムに基づくエコシステム内の既存のツールは強力な保証を提供しているが、一般的に使用するには専門知識が必要である。この新しいツールはLean4証明系とZ3のようなSMTソルバーを組み合わせて、コントラクトが意図したとおりに動作するかを自動的にチェックする。その目標は、開発者が自分で形式証明を記述する必要性をなくすことである。

…