Verifereum

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

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

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.