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

Slither is a Solidity and Vyper static analysis framework written in Python3. It runs a suite of vulnerability detectors, prints visual information about contract details, and provides an API to easily write custom analyses. Slither enables developers to find vulnerabilities, enhance their code comprehension, and quickly prototype custom analyses. Slither has been used for many years by both security engineers and developers to secure their smart contracts. By allowing developers to find the most common vulnerabilities on their smart contracts, Slither helps to improve the security of the Optimism ecosystem. Slither has 90+ detectors, and works on both Solidity and Vyper. In addition it provides printers, helping to review quickly features of contracts. It's python API can also be used to leverage its inbuilt analysis for custom needs. Slither can directly be run on a contract deployed on optimism, with slither optim:0x..ADDRESS

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.

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.