Formal verification 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. No formally verified protocol has been exploited, barring Sushi Swap, however, the exploit occurred in an unverified part of the contract.

Our formal verification teams will work in tandem with your engineering teams to define a formal specification detailing the behaviors of your smart contract. We will then formally verify that your implementation satisfies these specifications.

We currently offer interactive theorem proving (ITP) based approaches to formal verification and have an automated theorem proving (ATP) approach coming soon.

Interactive Theorem Proving (ITP)

We have a formalisation and powerful reasoning infrastructure in Lean for StarkNet smart contracts based on Prof. Jeremy Avigad’s formalisation of Cairo. It is able to reason about inter-contract invariants and dynamic properties of the system as a whole. This infrastructure is verified against the AIR implementation of the StarkNet ZKVM and is the ideal solution for our customers who need the highest degree of confidence.

We offer a bespoke formal verification service for StarkNet smart contracts. We will work to formally specify your protocol with your engineers and extend our formalisation as necessary to capture whatever properties you care about. Depending on the complexity of the specifications required, the protocol, the external dependencies, and the StarkNet language features used, the length of collaboration required may vary.