ConCert
A Coq framework for formal verification, property-based testing, and extraction of smart contracts.
What is ConCert?
ConCert is a framework for smart contract verification and development using the Coq proof assistant. It enables formal verification of contract correctness, property-based testing to find vulnerabilities, and extraction to executable blockchain languages. The framework helps prevent real-world attacks and ensures mathematical guarantees for decentralized applications.
Blockchain developers and researchers building high-assurance smart contracts, particularly those working on DeFi protocols or security-critical applications requiring formal verification.
ConCert provides an integrated toolkit for end-to-end smart contract verification—from formal proofs in Coq to extracted, executable code—offering stronger security guarantees than testing alone. Its property-based testing framework has successfully identified real-world vulnerabilities in major DeFi platforms.
Overview
A framework for smart contract verification in Coq
Use Cases
Best For
- Formally verifying correctness properties of smart contracts before deployment
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
