Builder-Tools

Solidity is an object-oriented, high-level language for implementing smart contracts.

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.

The Ethernaut is a community-driven capture-the-flag wargame that challenges developers of all levels to break smart contracts while learning common Solidity vulnerabilities. Maintained by OpenZeppelin, each level provides a gamified experience where a smart contract must be ‘hacked’ to progress. It is 100% open-source, with all levels contributed by players. In 2024, we have continued expanding the game, adding four new advanced levels—HigherOrder, Stake, Impersonator, and Magic Animal Carousel—which explore current vulnerabilities in smart contract development. These levels introduce challenges related to low-level EVM programming, staking vulnerabilities, signature verification exploits, and bitwise manipulation attacks, pushing players to deepen their understanding of Ethereum security. Beyond new levels, we have also redesigned the UI, added support for multiple networks, and expanded language translations to make the game more accessible to a global audience. We believe that The Ethernaut is an essential training tool for developers across the Ethereum ecosystem, including those building on the Optimism network. By continually evolving the game with new challenges and features, we strive to make smart contract security education engaging, practical, and accessible to everyone.