安全与测试hax形式化验证形式化验证网站 （在新标签页中打开）cryspen/hax(480 ☆) （在新标签页中打开）hax 是一个用于将 Rust 的大部分子集高保证地翻译成形式化语言（如 F* 或 Rocq）的工具。相关资源K Semantics of the Ethereum Virtual Machine (EVM)KEVM 是 EVM 的 K 框架可执行语义：当你需要一致性检查执行、符号探索、Gas 推理或密切跟踪以太坊规则的证明时，可以将其指向字节码。Kontrol - formal verification tool based on Foundry and KEVMKontrol 将 Foundry 属性测试提升为由 KEVM 支持的证明，以便你可以追求形式化保证，与单独使用原始 KEVM 相比，减少了手工编写规范的工作量。ActAct 是以太坊的声明式规范语言和工具链，用于描述 EVM 程序的所有行为，以便 SMT 求解器、定理证明器或经济分析工具能够推理字节码级别的正确性和激励兼容性，包括针对具体实现的自动求精证明。Certora AutoProverCertora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.VerifereumVerifereum 将以太坊智能合约连接到由 HOL4 支持的定理证明，因此当自动化的 SMT 方法不够用时，你可以瞄准非常强的正确性声明。Certora ProverCertora 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.
