🪁 coq-of-solidity
This project was funded by the Aleph Zero Foundation.
coq-of-solidity is a formal verification tool with interactive theorem proving 💫 for the 🪁 Solidity smart contract language.
It converts Solidity smart contracts to the 🐓 Coq proof assistant. It enables formal verification of Solidity smart contracts, that is to say code audits that cover all possible executions. The coq-of-solidity tool is open source. It makes the Coq translation from the Yul intermediate representation used by the Solidity compiler. The generated Coq code is more verbose than the source Solidity as it explicates low-level details of the execution model.
Formal verification with interactive theorem proving 💫 provides the highest level of security so it would be a big miss not to use it. This is the only way to ensure full protection even against state-level actors 🦸.
🦸 Contact us!Workflow
To formally verify a Solidity project using coq-of-solidity we work as follows:
- Translate the Solidity code to Coq using
coq-of-solidity - Define the state model of the contract (storage, memory, etc.)
- Write functional specifications for each function of the Solidity contract
- Verify that these specifications are equivalent to the translated Coq code
- Prove properties over these specifications
Some of this work can be verbose and repetitive, but tools like Github Copilot are increasingly helpful for generating boilerplate code and specifications.
Benefits
- Comprehensive security: Formal verification covers all possible inputs and execution paths.
- Reusable proofs: Verification can be re-run as the contract evolves.
- Higher assurance: Provides mathematical guarantees beyond traditional testing and auditing.