Presentation

Here is a 🏎️ quick presentation, in simple words, of what coq-of-solidity does.

With coq-of-solidity you make sure that the money stored on your Solidity smart contract cannot be stolen. 🛡️

Every month, millions of dollars 💰 are stolen from smart contracts. This is because a single mistake in the code, even if this is just one line, lets an attacker withdraw all the money and disappear with it!

Audits are mandatory, but this is a human 🧠 verifying the code, and mistakes are made.

🚨 Even if major smart contracts have all been audited, they are still regularly hacked.

With coq-of-solidity, the computer checks that the reasoning of the auditor is correct: this is like a spell checker for auditors.

As a result, you can truly be sure that no attack scenario has been forgotten and that your smart contract is truly secure ✅.

In addition, when you update the code of your smart contract, you can replay the reasoning for free to make sure your smart contract is still secure on the old part 😎 . This saves on auditing costs.

Why us?

Verifying reasoning about code is called 🔎 formal verification. This is a complex technique 🧪 and very few companies have developed a tool to do this for Solidity. In addition, coq-of-solidity is the only one with Clear that can express any possible reasoning/property on your code. This is thanks to the use of an 🐓 interactive theorem prover on the backend.

At 🌲 Formal Land, where we developed coq-of-solidity, we are one of the leading teams applying formal verification to large-scale programs. We have developed two other formal verification tools, with coq-of-rust for 🦀 Rust and coq-of-ocaml for 🐫 OCaml. Read more about what we do on our 📖 blog.

How much? 💸

For a large smart contract (5,000 lines of Solidity), consider a price of $50,000 for a formal verification of a model of the code, and $100,000 for a verification at the level of the source code (more precise). So, this is competitive with traditional audits in terms of pricing.

💌 Contact us for an evaluation!

coq-of-solidity is fully open-source, under MIT licence, so you can also use it by yourself! 🚀