certora

Certora

Certora was founded in 2018 that specializes in formal verification tools for smart contracts on blockchain platforms, particularly Ethereum. They provide automated tools that help developers detect and prevent bugs and vulnerabilities in smart contract code before deployment.

Overview

Certora's flagship product, the Certora Prover, allows developers to write formal specifications for their smart contracts. The Prover then automatically verifies that the contract code adheres to these specifications, ensuring that the smart contracts behave as intended. This helps mitigate risks associated with smart contract vulnerabilities.

History

Founded by Professor Mooly Sagiv, an expert in program analysis and formal methods, Certora was established to bridge the gap between academic research in formal verification and practical tools for the blockchain industry. The company's leadership includes professionals with extensive backgrounds in computer science, formal methods, and cybersecurity.

Technology

Certora's technology leverages formal methods—a mathematical approach to software verification—to ensure smart contract correctness. Key aspects of their technology include:

• Certora Prover: An automated tool that checks whether smart contracts comply with specified rules and properties. Developers write these rules in a domain-specific language provided by Certora.
• Domain-Specific Language (Certora Specification Language): Allows developers to express complex properties and invariants that the smart contracts must satisfy.
• Integration with Development Workflows: The Prover can be integrated into continuous integration/continuous deployment (CI/CD) pipelines, enabling ongoing verification as the code evolves.
• Support for Solidity: Designed to work with Solidity, the most widely used programming language for Ethereum smart contracts.

Products and Services

• Certora Prover: Enables automated formal verification of smart contracts.
• Security Audits: Professional services offering in-depth analysis and verification of smart contract code.
• Training and Consulting: Provides education and support to development teams on adopting formal verification practices.

Use Cases

Here are several protocols using Certora's products:

• Compound: Used Certora Prover to verify the correctness of their interest rate protocols.
• Aave: Employed Certora's technology to ensure the security of their lending and borrowing platforms. In a discussion on the Aave Governance Forum titled "Continuous Formal Verification," Aave considered implementing ongoing formal verification processes using Certora's tools. By integrating continuous formal verification into their development workflow, Aave aims to enhance the robustness and reliability of its decentralized finance platform. This approach helps identify and mitigate potential vulnerabilities in smart contract code before deployment, safeguarding user assets and maintaining trust in the protocol.
• MakerDAO: Leveraged Certora's services to validate the stability mechanisms of their decentralized stablecoin system.
• Synthetix: Implemented formal verification to secure their synthetic asset issuance platform.

Partnerships and Collaborations

Certora has established partnerships with major entities in the blockchain ecosystem:

• Ethereum Foundation: Collaborated on initiatives to improve smart contract security.
• OpenZeppelin: Worked together to integrate formal verification into widely used smart contract libraries.
• Academic Institutions: Engaged in research projects to advance the application of formal methods in blockchain technology.

Aave Security

https://governance.aave.com/t/continuous-formal-verification/6308