安全、测试与形式化验证

我们是 Runtime Verification，一家研发公司，致力于构建严谨的工具以确保关键系统的安全性和正确性。我们的团队开发了 KEVM，这是以太坊虚拟机 (EVM) 最完整、经过实战检验的形式化语义，用 K Framework 编写。 KEVM 不仅仅是一个规范，它是一个可执行的规范，可用于对智能合约进行符号推理、运行一致性测试、分析 gas 使用情况、调试程序以及形式化验证正确性属性。它通过了完整的以太坊测试套件，并用于验证高价值合约，包括 Solidity 和 Vyper 中的 ERC-20 代币。我们最近更新了语义以支持 Pectra 升级。 KEVM 正被 Kontrol 积极使用——这是我们的 Solidity 形式化验证工具，被 EVM 生态系统中的领先团队积极使用，包括 Optimism、以太坊基金会、Lido、Uniswap，以及更广泛的以太坊社区的安全研究人员和审计员。 我们积极维护此存储库，为以太坊的协议演进做出贡献，并与 Foundry 等开发者工具集成。通过 KEVM，我们正在突破可证明正确和安全的智能合约基础设施的界限。

Act 是一种用于形式化验证的智能合约规范语言和工具包。Act 规范是对 EVM 程序所有可能行为的形式化、高级描述。Act 允许利用许多现有的通用验证工具来证明有关规范的属性。此类工具包括 SMT 求解器（cvc5、z3、bitwuzla）、定理证明器（Coq）和经济分析工具（CheckMate、Open Games）。Act 规范可以自动证明等同于 EVM 中的具体实现。对于非常简单的合约，可以从 EVM 字节码自动生成 Act 规范。 这是一个端到端的管道，支持对 EVM 字节码的高级属性进行有原则的推理。它支持对正确性（例如会计不变量）和经济属性（例如激励相容性）的推理。Act 规范作为一种高级智能合约表示，允许将现有的通用分析和验证工具轻松集成到 EVM 环境中。

Titanoboa 是一个 Vyper 解释器和测试框架，为 Vyper 智能合约提供现代、集成的开发体验。它使开发者能够直接在 Python 中测试和调试 Vyper 合约，提供漂亮的追溯、分叉、调试功能、pytest 集成和开箱即用的模糊测试等功能。除了其独立功能外，Titanoboa 还是 Ape 和 Moccasin 等其他流行测试框架的基础，并且是 Vyper 生态系统的核心基础设施。