安全与测试

hax

形式化验证

hax 是一个用于将 Rust 的大部分子集高保证地翻译成形式化语言（如 F* 或 Rocq）的工具。

相关资源

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol 将 Foundry 属性测试提升为由 KEVM 支持的证明，以便你可以追求形式化保证，与单独使用原始 KEVM 相比，减少了手工编写规范的工作量。

Act

Act 是以太坊的声明式规范语言和工具链，用于描述 EVM 程序的所有行为，以便 SMT 求解器、定理证明器或经济分析工具能够推理字节码级别的正确性和激励兼容性，包括针对具体实现的自动求精证明。

Verifereum

Verifereum 将以太坊智能合约连接到由 HOL4 支持的定理证明，因此当自动化的 SMT 方法不够用时，你可以瞄准非常强的正确性声明。