Certora

Certora develops formal verification tools for smart contracts. Its main product, Certora Prover, analyzes smart contract bytecode against formal specifications (rules) written by developers describing expected behavior. The tool systematically checks all possible contract states and execution paths to identify vulnerabilities and logic errors that traditional testing methods may miss. The Certora Prover can be integrated into development pipelines to run automatically on every code commit, allowing continuous verification of smart contract code as it changes. In addition to the automated tool, Certora offers services from its team of formal verification experts, who can be hired to write custom specifications and rules tailored to a client's codebase. Certora also engages the broader security community through audit contests run in partnership with platforms such as Code4rena, crowdsourcing the creation of formal specifications to identify vulnerabilities in client code. The company's customers are primarily decentralized finance (DeFi) protocols and blockchain projects, including MakerDAO, Lido, Balancer, Aave, Compound, Coinbase, and the Ethereum Foundation. Certora states that the protocols it has worked with collectively secure more than $100 billion in total value locked (TVL).