A friendly framework to formally verify zero-knowledge systems
Zero-knowledge applications are one of the most anticipated innovations in the blockchain space. They allow the scaling of transactions almost indefinitely and preserve the privacy of user information.
One issue is that these systems are very complex. Testing alone cannot ensure the security of these systems, and billions worth of assets will be at risk.
Formal verification, based on a mathematical analysis of the code, is the solution to ensure the safety of such systems.
With Garden, we are building a friendly, open-source, Rocq framework to formally verify zero-knowledge systems.
We are first targeting the two following circuit formats:
- Circom
- Mina-like Rust circuits like in keccak/interpreter.rs
To ensure your circuits are correct, down to the implementation level, please contact us at contact@formal.land!
We provide formal verification services as well as training and custom developments.
To make safe cryptography available to everyone, we will be hosting training sessions on this website: https://cryptography.academy/
Here are some related projects:
You can make a pull request to add yours!