Skip to main content

6 posts tagged with "coq-of-ocaml"

View All Tags

ยท 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


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 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.