Formal Land

We develop a solution to formally verify ink! smart contracts (using mathematical methods to check the code at 100%).

Our aim is to provide a tool to formally verify ink! smart contracts, that are written in the Rust language. Formal verification is about using mathematical methods to exhaustively safety properties and specifications of a program. This is a key step to ensure the security of critical code such as smart contracts. The formal verification landscape for Rust is still young. We are developing our tool coq-of-rust to verify Rust code
by translation to the proof assistant Coq. This is the technique we used to verify the code of the crypto-currency Tezos, composed of over 100,000 lines of OCaml code. We believe this can scale for the verification of Rust code as well. Our first milestone is to support enough of the Rust language to be able to analyze the ERC-20 implementation and to prove its safety properties. Next, we want to stabilize our tool to also verify four other examples of ink! smart contracts.