Solutions across three main areas
We are also working on developing a robust infrastructure for EVM/Yul-based smart-contract verification, relying on our in-house Clear interactive verification framework and other state-of-the-art verification tools.
zk-circuits
We formally verify properties of your zk-circuits in the Lean proof assistant by extracting appropriate information from your zk-circuit Domain Specific Language (DSL).
zk-related cryptography
We formally verify, using cutting-edge tools, that your zk-related infrastructure satisfies the desired cryptographic security properties.
Protocol modelling
We construct a mathematical model of your protocol in the Lean proof assistant and formally verify that it satisfies the desired security properties.




























