Skip to main content

ยท 5 min read

We are diversifying ourselves to apply formal verification on 3๏ธโƒฃ new languages with Solidity, Rust, and TypeScript. In this article we describe our approach. For these three languages, we translate the code to the proof system ๐Ÿ“ย Coq. We generate the cleanestย ๐Ÿงผ possible output to simplify the formal verificationย ๐Ÿ“ effort that comes after.

Formal verification is a way to ensure that a program follows its specification inย ๐Ÿ’ฏ% of cases thanks to the use of mathematical methods. It removes far more bugs and security issues than testing, and is necessary to deliver software of the highest qualityย ๐Ÿ’Ž.

ยท 2 min read

Here we recall some blog articles that we have written since this summer, on the formal verification of the protocol of Tezos. For this project, we are verifying a code base of around 100,000 lines of OCaml code. We automatically convert the OCaml code to the proof system Coq using the converter coq-of-ocaml. We then apply various proof techniques to make sure that the protocol of Tezos does not contain bugs.

ยท 4 min read

Elephants

Our primary goal at Formalย Landย ๐ŸŒฒ is to make Tezos the first crypto-currency with a formally verified implementation. With formal verification, thanks to mathematical methods, we can check that a program behaves as expected for all possible inputs. Formal verification goes beyond what testing can do, as testing can only handle a finite amount of cases. That is critical as cryptocurrencies hold a large amount of money (around $3B for Tezos today). The current result of our verification project is available on nomadic-labs.gitlab.io/coq-tezos-of-ocaml. Formal verification is also key to allowing Tezos to evolve constantly in a safe and backward compatible manner.

ยท One min read

Recently, we added two new blog posts about the verification of the crypto-currency Tezos:

We also talked at the Lambda Lille Meetup (in French) to present our work on coq-of-ocaml for Tezos. A video on the Youtube channel of the Meetup should be available shortly. We thanks the organizers for hosting the talk.

ยท One min read

Welcome to the blog of Formal Land. Here we will post various updates about the work we are doing.