Formal verification service

The total TVL of the crypto ecosystem is $53 billion, of which there were $1.19 billion in losses due to exploits from January to July 2022 alone. Formal verification can catch these flaws before your smart contract is deployed.

Solutions across three key areas

ZK-circuit verification

ZK-circuits are part of the Zero-Knowledge Proof process which allows one party to prove the truth of a statement to another party without disclosing any information about it. We use extractions from different zk-circuit Domain Specific Languages (DSLs) into Lean 4 proof assistant to verify zk-circuit properties formally.

EVM-based smart contract verification

EVM-based smart contract verification involves using formal methods to prove the correctness, security, and adherence to formal specifications of an EVM smart contract.

Starknet smart contract verification

Starknet smart contract verification involves using formal methods to prove the correctness, security, and adherence to formal specifications of a Starknet smart contract.

We are RISC Zero’s verification partner

RISC Zero is building the RISC Zero zero-knowledge virtual machine (zkVM) as a major step toward improving the security and trustworthiness of distributed applications.

Nethermind recently partnered with RISC Zero to develop tooling that formally verify their zk-circuit against the RISC-V semantics.

Formal verification, specification and tooling

We offer a range of formal verification and specification categories, with varying levels of security. Our team will guide you to a formal verification and specification service that best suits your projects needs.

Formal verification, specification and tooling

We offer a range of formal verification and specification categories, with varying levels of security. Our team will guide you to a formal verification and specification service that best suits your projects needs.

Formal verification, specification and tooling

We offer a range of formal verification and specification categories, with varying levels of security. Our team will guide you to a formal verification and specification service that best suits your projects needs.

Past and current clients

Starkware

StarkWare is using STARK proofs to bringing scalability, security and privacy to a blockchain near you.

ZKLend

zkLend is a protocol combining zk-rollup scalability, superior transaction speed, and cost-savings with Ethereum's security.

Past and current clients

Get in touch!

We recognize that applications of formal verification within the web3 ecosystem are rapidly evolving, and we are interested in exploring any proposals you may have.

If you have formal verification needs outside of the Starknet ecosystem, get in touch and let's discuss what we can do for you.

Collaborating on this project

Julian

Sutherland

František

Silváši

Ilia

Vlasov

Collaborating on this project

Julian

Sutherland

František

Silváši

Ilia

Vlasov