# 🪁 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.

We apply `coq-of-rust`

to **formally verify your Solidity programs** for **$10 per line of verified code** (excluding comments). 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 🦸.

We always verify the first 100 lines for free 🎁.

## 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.