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

We are Runtime Verification, a research and development company building rigorous tools to ensure the safety and correctness of critical systems. Our team has developed KEVM, the most complete and battle-tested formal semantics of the Ethereum Virtual Machine (EVM), written in the K Framework. KEVM is not just a specification, it is an executable specification that can be used to symbolically reason about smart contracts, run conformance tests, analyze gas usage, debug programs, and formally verify correctness properties. It passes the full Ethereum test suite and is used to verify high-value contracts, including ERC20 tokens in both Solidity and Vyper. We recently updated the semantics to support Pectra upgrade. KEVM is being actively utilized by Kontrol - our formal verification tool for Soldiity, which is actively used by leading teams in the EVM ecosystem, including Optimism, Ethereum Foundation, Lido, Uniswap, as well as security researchers and auditors across the broader Ethereum community. We actively maintain this repository, contribute to Ethereum’s protocol evolution, and integrate with developer tooling like Foundry. Through KEVM, we are pushing the boundaries of what’s possible in provably correct and secure smart contract infrastructure.

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.

solidity-coverage provides smart-contract code coverage for the Hardhat developer platform. It's highly accurate, supports full viaIR solidity compilation and a large set of solidity-specific code branch patterns. It's installed on ~230k Github projects and is downloaded ~100k times a week from NPM.