Code repositories, projects, and practical examples using Kontrol
Here are notable projects and code repositories that use Kontrol for formal verification. These provide practical examples and templates for different use cases.
Optimism uses Kontrol to verify critical components of their Bedrock contracts. Their setup includes:
Custom deployment sequence for Kontrol proofs
Automated proof generation and verification
Integration with their CI pipeline
Comprehensive documentation of their verification process
Kontrol-Solady is a formal verification project for the Solady library, demonstrating how to verify commonly used smart contract patterns and optimizations.
Lido's Dual Governance uses Kontrol for formal verification of their dual governance mechanism.
Kontrol Demo is a simple repository demonstrating basic Kontrol usage, perfect for getting started with formal verification.
Uniswap Hooks Proofs provides formal verification proofs for secure and modular Uniswap hooks. A detailed walkthrough of these proofs is available in the Verified Hooks workshop video.
The Secureum Kontrol Workshop provides hands-on examples and exercises for learning Kontrol, including:
Basic verification examples
Advanced proof techniques
Common patterns and best practices
Kontrol DSS 2024 showcases more advanced usage patterns and verification techniques.
To explore these examples:
Start with the Kontrol Demo for basic usage
Review the Secureum Workshop for hands-on learning
Study the Optimism implementation for production usage
Explore Kontrol-Solady for library verification patterns
Each project provides unique insights into how Kontrol can be used effectively in different contexts and for different purposes.
Looking for learning materials instead? Check out our Resources page for videos, blog posts, and educational content.
Last updated
Was this helpful?
Was this helpful?
