Verifereum

KEVM 是 EVM 的 K 框架可执行语义：当你需要一致性检查执行、符号探索、Gas 推理或密切跟踪以太坊规则的证明时，可以将其指向字节码。

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.