Use
Kontrol is an open-source, free-to-use tool. You can start verifying for free now.
$0/ free
- Symbolic execution for Solidity contracts
- Turn Foundry tests into formal proofs
- Run proofs locally
- No need to learn new semantics or a new language
Formal verification
The highest security assurance available for a codebase
Instead of just looking for bugs, verify that your implementation adheres to its specification across the entire input space.
Ways to work with us
Run it yourself, run it with us, or hand it over.
Consult
Most popularLet us set up the tools on your codebase, teach you how to use them, and write tests and lemmas with you.
$30k/ month
- One full-time engineer dedicated to your project, with the whole formal methods team in support
- We set up Kontrol and remote compute for your project
- Advice on writing proofs and improving specifications
- Help writing lemmas for Foundry tests
Outsource
We produce the specifications and run formal verification for you.
$50k/ month
- Two full-time verification engineers
- Symbolic execution of proofs enabled in your CI
- Support through the development lifecycle
- Applicable pre- or post-implementation
Common questions
Formal methods mean better security and cheaper audits.
- How is testing the entire input space possible?
- Symbolic execution allows exploring all possible execution paths in a program by using symbolic values instead of concrete data. This ensures every potential input is considered, surpassing traditional fuzzing methods that rely on random inputs.
- Is it difficult?
- It is not much more complex than writing Foundry tests. Our team can help streamline the process, teaching your developers to master formal methods quickly. Proofs are written in Solidity!
- Is it expensive?
- No! Engineer time to set up Kontrol and write proofs is cheaper than traditional audit rates. Plus, having rock-solid, formally verified specifications simplifies the audit process. Formal Verification integrated into your CI helps ensure that the code is correct as it evolves, providing continuous security assurance.
- Why formally verify?
- Formal verification ensures a holistic approach to security, leading to better system design and solid implementation. It catches edge cases early, integrating security from the start rather than as an afterthought.
Formal methods development cycle
Six steps, from plain English to a verified contract.
- 1
Mechanism Design
Outline the system in plain English
- 2
Define Specifications
Develop formal specifications from the design.
- 3
Implement
Write the smart contracts based on the specifications.
- 4
Execute Symbolically
Test the implementation against the formal specifications.
- 5
Iterate
Refine the implementation to fix bugs and address edge cases.
- 6
Streamline Audit
Deliver well-polished, formally verified smart contracts to auditors, bug bounties, and contests.
Teams we have formally verified for
Ready to prove your contracts correct?
Request a demo