Kontrol
  • Overview
    • Kontrol
      • The significance
      • Installations
  • Guides
    • Proofcast Episode: Getting Started
    • Kontrol Example
      • Property Verification using Kontrol
      • K Control Flow Graph (KCFG)
      • Proof Management
      • Debugging a Proof
    • Node Refutation
    • Bytecode Verification
    • Advancing Proofs
      • KEVM Lemmas
      • Writing Simplifications
      • Rule Application
      • Symbolic Storage
  • Cheatsheets
    • Kup Cheatsheet
    • Kontrol Cheatsheet
    • Cheatcodes
  • Tips
    • Debugging Failing Proofs
  • Glossary
    • Kontrol Arguments
    • Kontrol Build Options
    • Kontrol Prove Flags
  • Developer Docs
    • Digest File
  • Learn More
    • Resources
    • Example Projects
  • 🔗Links
    • Join our Discord!
    • Kontrol Repo
    • Gitbook Repo
Powered by GitBook
On this page
  • Production Projects
  • Optimism
  • Solady
  • Educational Resources
  • Patrick Collins' Course
  • Secureum Workshop
  • Example Repositories
  • Kontrol Demo
  • DSS 2024
  • Getting Started

Was this helpful?

Edit on GitHub
  1. Learn More

Example Projects

Real-world projects and examples using Kontrol

PreviousResources

Last updated 24 days ago

Was this helpful?

Here are some notable projects and examples that use Kontrol for formal verification:

Production Projects

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

Solady

is a formal verification project for the Solady library, demonstrating how to verify commonly used smart contract patterns and optimizations.

Educational Resources

Patrick Collins' Course

includes Kontrol examples as part of their curriculum, showing how to use formal verification to prevent common vulnerabilities.

Secureum Workshop

  • Basic verification examples

  • Advanced proof techniques

  • Common patterns and best practices

Example Repositories

Kontrol Demo

DSS 2024

Getting Started

To explore these examples:

Each project provides unique insights into how Kontrol can be used effectively in different contexts and for different purposes.

The provides hands-on examples and exercises for learning Kontrol, including:

is a simple repository demonstrating basic Kontrol usage, perfect for getting started with formal verification.

showcases more advanced usage patterns and verification techniques.

Start with the for basic usage

Review the for hands-on learning

Study the for production usage

Explore for library verification patterns

Optimism
Kontrol-Solady
Cyfrin's Smart Contract Exploits Course
Secureum Kontrol Workshop
Kontrol Demo
Kontrol DSS 2024
Kontrol Demo
Secureum Workshop
Optimism implementation
Kontrol-Solady