Cardanoノードで実行されるスマートコントラクトを実際のレベルで形式検証することが可能になり、抽象モデルや表層ループで推論するのではなく、UPLC（Untyped Plutus Core）を直接操作することができるようになった。 

UPLCを直接対象とすることで、ソース言語を問わずコントラクトの検証が可能になる。これには、Plinth、Aiken、Plutarchの他、Plutus Coreコンパイルパイプラインを対象とする将来の言語も含まれる。

UPLCレベルにおけるここまでの証明自動化と分析は、これまでCardanoで実現されたことはない。 

…

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

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

…