Certora AutoProver

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.

Kontrol 將 Foundry 屬性測試提升為由 KEVM 支援的證明，因此您可以追求形式化保證，而所需的手寫規範工作比單獨使用原始 KEVM 更少。