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
  • Videos
  • Blogs and Other Resources

Was this helpful?

Edit on GitHub
  1. Learn More

Resources

If you want to learn more or get involved

Join the Community on Discord! If you have questions, feedback, or problems we would love to hear from you and offer support.

Videos

  • In Solidity Specification, Testing, and Verification

  • Tackling Rounding Errors with Precision Analysis

  • Formal Methods for the Working DeFi Dev

  • Security: Auditing and Formal Methods

  • Towards Adoption of Symbolic Execution for DeFi Security

  • K, KEVM, Kontrol presentation video

Blogs and Other Resources

  • Using Foundry to Explore Upgradeable Contracts (Part 1)

  • Foundry: Gen 2 of Ethereum Tooling

  • To learn more about Foundry check out the Foundry Book

  • KEVM and Kontrol are powered by the K Framework, if you are interested in learning more check out the 0 to K Tutorial

  • We also have formal verification on Algorand powered by K! Check out KAVM!

Did you see a typo somewhere in the Gitbook? Click the three dots on the page to suggest an edit on Github!

PreviousDigest FileNextExample Projects

Last updated 1 year ago

Was this helpful?