76%

The Certora Prover provides complete path coverage for a set of safety rules provided by the user. The prover either guarantees that a rule holds on all paths and all inputs or produces a test input that demonstrates a violation of the rule. A traditional security audit usually involves a manual, holistic review of an entire system. Formal verification, on the other hand, produces a proof that a piece of software satisfies a specification. The Certora team is available for formal verification projects to write specifications and verify the code against these specifications. Often, verification projects find bugs in the code, and these bugs can be fixed during the course of the project, with the fixes proved correct. The team also produces a report describing the properties verified and bugs discovered. At the moment, we only analyze and review Ethereum bytecode. Certora doesn’t have a token yet.