Безопасность, тестирование и формальная верификация

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.

Titanoboa is a Vyper interpreter and testing framework that provides a modern, integrated development experience for Vyper smart contracts. It enables developers to test and debug Vyper contracts directly within Python, offering features like pretty tracebacks, forking, debugging capabilities, pytest integration and out-of-the box fuzzing. Beyond its standalone capabilities, Titanoboa serves as the foundation for other popular testing frameworks like Ape and Moccasin, and is a core piece of infrastructure for the Vyper ecosystem.

Runtime Verification has been at the forefront of open-source formal verification tools for more than a decade. Our generalistic approach allows us to use our technology on multiple blockchains. While KEVM offers our verification infrastructure to all EVM-based smart contracts, Kontrol greatly reduces the barrier to entry to formal verification for Solidity smart contracts. Our tooling is completely open source and freely accessible to all developers of the Optimism ecosystem at no additional cost. KEVM is an EVM executable formal semantics written in the K framework. KEVM passes all Ethereum conformance tests and is the entry point for formally verifying smart contracts with the K framework. However, using plain KEVM requires ad-hoc training on the K framework to write specifications. Additionally, these specifications can be quite verbose, increasing the difficulty of writing them. Kontrol solves this by allowing developers to write the formal specification of their smart contracts directly as Foundry property tests. These tests are automatically translated into KEVM specifications, keeping all the verification guarantees whilst allowing for a much more easy developer experience.