Formal Verification grants developers the highest security assurance. Instead of just looking for bugs, verify that your implementation adheres to specs for the entire input space.
Use
Kontrol is an open-source free-to-use tool. You can start verifying for free now.
Formal methods mean better security, 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 secruity 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
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.
