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.