“Certora’s technology helped to cover security on decentralized Aave Protocol, essentially finding vulnerabilities that are usually difficult to find in manual code reviews and audits. When building mission-critical software such as financial technology, Certora is a must.”
“Formal verification from Certora is the most powerful tool we have to ensure that we are building a secure, impenetrable system -- the top priority for any serious smart contract developer."
“Certora has been a crucial partner along Balancer's journey to ensure excellence in our code quality/security"
“Certora has been a critical security partner in Stakehouse Protocol’s formalization efforts. We are consistently impressed by the team’s hands-on approach and their Certora Prover tool efficacy. It reinforces the key mechanisms while giving clarity and adversarial simulation for our Multichain ETH scenarios.”
"Certora gives us so much peace of mind as we develop smart contracts at Syndicate. With formal verification running on every single commit, we can maintain a fast development velocity without decreasing security."
“Certora has unlocked TrustToken’s ability to iterate quickly while maintaining confidence in the security of our smart contracts. Our team has discovered and fixed numerous unintended bugs thanks to this powerful tool.”
"Certora has given us the ability to practically apply formal verification methods to anything we do on-chain. They have an excellent team who we've partnered with closely over the years, and the process of writing invariants with them has proven to be invaluable in writing better smart contracts."
“The Certora prover plays an important role in our overall safety strategy by providing an accessible way to quickly iterate on formal specifications and determine the correctness of bytecode. It's what we reach for when both time and safety are of the essence. Engineers can learn to use it in a few days and don't need a Ph.D. in formal methods to create good specifications. The tool recently helped us to uncover an inconsistency in an updated version of one of our oldest smart contracts, which was a surprising result. The Certora team is highly responsive and promptly addresses issues we encounter.”
Lido is a family of open-source peer-to-system software tools deployed and functioning on the Ethereum, Solana, and Polygon blockchain networks. The software enables users to mint transferable utility tokens, which receive rewards linked to the related validation activities of writing data to the blockchain, while the tokens can be used in other on-chain activities.
MakerDAO enables the generation of Dai, the world’s first unbiased currency and leading decentralized stablecoin. Dai is a stable, decentralized currency that does not discriminate. Any individual or business can realize the advantages of digital money.
Syndicate enables scalable on-chain infrastructure and is backed by a16z, IDEO CoLab Ventures, Variant, Electric Capital, and over 100 other investors and strategic partners.
Balancer is a protocol for programmable liquidity. It allows for the creation of self-balancing liquidity pools with flexible parameters. A pool can have 2 or more tokens and each token can have different weights. Balancer also allows for smart pools which have evolving parameters: think of a surge pricing liquidity pool that increases the trading fees in times of high volatility/demand for liquidity.
Aave Protocol is a decentralized, open-source, and non-custodial money market protocol. Depositors can deposit assets into the protocol and earn interest on their deposits without relying on middlemen.
Compound is a transparent, autonomous money market — allowing users & applications to frictionlessly earn interest or borrow Ethereum assets without relying on a counterparty.
Silo is a risk-isolating lending protocol that implements permissionless lending markets where any token can borrow another. Silo is secure by design – each lending market supports two assets only, the bridge asset and a unique token asset. This design concentrates liquidity in single pools and allows for efficiency.
Morpho is a Peer-to-Peer (P2P) layer on top of lending pools like Compound or Aave. Rates are seamlessly improved for both suppliers and borrowers whilst preserving the same liquidity and market risk guarantees.
✓ To learn how to use the Certora Prover, see our Quick guide.
✓ In our webinars, Dr. James Wilcox presents the basics of Formal Verification and shows the Certora Prover in action, and Prof. Mooly Sagiv explains the technology underlying the Certora Prover.
Hybrid / Israel
Certora is developing cutting edge tools for guaranteeing software correctness.
We are looking for front end developer that will develop our user-facing features, and work closely with the rest of the development group and product group to deliver easy-to-use solutions to our users – developers, and auditors in the web3 world.
This is exactly the intended use case of the Certora prover!
The Certora Prover provides complete path coverage for a set of safety rules provided by the user. For example, a rule might check that only a bounded number of tokens can be minted in an ERC20 contract. 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.
The problem addressed by the Certora Prover is known to be undecidable. This means that there will always be pathological programs and rules for which the Certora prover will time out without a definitive answer. Our experience so far is that realistic customer’s programs are not pathological and can be successfully analyzed by the Prover. The Certora team is actively working to reduce the number of timeouts when analyzing smart contracts of customers.
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.
Definitely, and we will assist you and review your rules for free.
The Certora Prover takes as input the smart contract (either as EVM bytecode or Solidity source code) and a set of rules, written in Certora’s specification language. The Prover then automatically determines whether or not the contract satisfies all the rules. Just as good testing sometimes requires code refactoring, verification occasionally requires changes to the code. For example, because the verification happens via the public API to the contract, some state pieces may need to have getters added so that they are accessible.
When the Certora Prover provides a test input that violates the rule, the user can check if this violation is due to a bug in the code or the verification rule. We also suggest performing a sanity check on the rules, e.g., by mutating the contract by adding an artificial bug and checking if any rule is violated. If no violations were found, the specification is missing a rule. The Certora Prover also automatically generates test cases for showing that a point in the program is reachable.
Unlike symbolic execution tools which select specific paths and a fixed set of bad patterns, such as MythX and Slither, the Certora Prover provides complete coverage for a user provided set of rules. Interactive theorem provers such as Coq and K can be used for interactively showing that a specific contract is correct. SMTChecker by the Solidity team and Verisol by Microsoft Research are similar to the Certora Prover in many respects but target Solidity sources with per program user assistance. This makes the tools hard to integrate into the CI pipeline --- the value of the verification is that it allows to move fast and break nothing!