Kontrol - formal verification tool based on Foundry and KEVM

KEVMは、EVMのKフレームワークの実行可能なセマンティクスです。適合性がチェックされた実行、シンボリックな探索、ガスの推論、またはイーサリアムのルールを厳密に追跡する証明が必要な場合は、これをバイトコードに向けます。

haxは、Rustの大部分をF*やRocqなどの形式言語に高保証で変換するためのツールです。

Actは、EVMプログラムのすべての動作を記述するためのイーサリアムの宣言型仕様言語およびツールチェーンです。これにより、SMTソルバー、定理証明器、または経済分析ツールは、具体的な実装に対する自動的な詳細化証明を含め、バイトコードレベルの正確性とインセンティブの互換性について推論できます。

Verifereumは、イーサリアムのスマート・コントラクトをHOL4を利用した定理証明に接続するため、自動化されたSMTアプローチでは不十分な場合に、非常に強力な正確性の主張を目指すことができます。