Certora

A formal-verification firm that produces machine-checked proofs of smart-contract invariants.

[[Formal-verification]] catches a class of bugs traditional audits miss — Certora has worked with Aave, Compound, MakerDAO, and Lido. Their reports cite specific invariants proved (e.g., "totalSupply equals sum(balanceOf) at all states reachable from the deployed bytecode").

Related terms

Formal verificationMathematical proof that a smart contract satisfies stated invariants under all reachable program states.
Audit reportA security firm's written review of smart-contract code, classifying findings by severity and tracking issuer responses.