Tools
We develop open-source tools to translate programs from various languages to the Rocq proof assistant, enabling full formal verification of your code without risks of errors in the translation.
Thanks to the use of interactive theorem proving, we can verify arbitrary security properties, including:
- High-level properties (determinism, access control, etc.)
- Complex maths (cryptography, etc.)
- Cross-language properties (inter-contract calls, etc.)
🦀 rocq-of-rust
rocq-of-rust translates Rust programs to Rocq for formal verification.
Funded by: Ethereum Foundation and Aleph Zero Foundation
🪁 rocq-of-solidity
rocq-of-solidity provides formal verification for Solidity smart contracts. It works by translating the Yul intermediate representation to Rocq.
Funded by: Aleph Zero Foundation
🌱 Garden for ZK
Garden is a framework for verifying zero-knowledge applications. It provides tools and libraries to formally verify ZK circuits, including support for Circom, Plonky3, and LLZK.
Funded by: Ethereum Foundation
🐫 coq-of-ocaml
coq-of-ocaml transpiles OCaml programs to Rocq. It was originally developed for the Tezos blockchain and has been used to verify over 100,000 lines of OCaml code. It supports advanced features like functors, first-class modules, and GADTs.
Funded by: French Government and Tezos Foundation
◼️ rocq-of-noir
rocq-of-noir enables formal verification of Noir zero-knowledge programs. It converts Noir code to Rocq after the monomorphization phase of the compiler.
Contact
Need help getting started with formal verification? Email us or schedule a call.