Act is a smart contract specification language and toolkit for formal verification. Act specifications are a formal, high-level description of all possible behaviours of an EVM program. Act allows many existing general purpose verification tools to be leveraged to prove properties about the specification. Such tools include SMT solvers (cvc5, z3, bitwuzla), theorem provers (Coq) and economic analysis tooling (CheckMate, Open Games). Act specifications can be automatically proved equivalent to concrete implementations in EVM. For very simple contracts, Act specifications can be automatically generated from EVM bytecode. This is an end-to-end pipeline that supports principled reasoning about high level properties of EVM bytecode. It supports reasoning about both correctness (e.g. accounting invariants) and economic properties (e.g. incentive compatibility). Act specifications serve as a high-level smart contract representation, allowing for easy integration of existing general purpose analysis and verification tooling into the EVM context.
安全性、测试和形式验证
Act
教育 · 分析 · 形式验证 · 符号执行
