Software reliability with proofs

‍

Making sure that a computer program behaves as expected, especially in critical applications (blockchain, smart contracts, energy, communications, etc.), is becoming more and more important. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite?  To express with exactness what is the expected behavior of a program, one first needs to use some formal logical language.

‍

A "formal proof" is a mathematical proof that is written in a language similar to a programming language. Formal proofs are harder for a human to read, but easier for a program to read. The advantage is that formal proof can be verified by a program, eliminating human error.

There is no program that can decide whether any property is true or not. However, we can have a program that decides whether any proof is correct or not, and there is such a program like that, namely Coq, to formally prove the correctness of some particular program.

Writing a program in Coq is not a straightforward task; it involves the knowledge of understanding the logic behind Coq, and that can make the task of writing proofs complex. This is the reason why, at Marigold, we have a formal verification team that is dedicated to exploring a new way that will help the process of writing such a program easier.

‍

Easier-proofs is a tool that is written in OCaml. The purpose of this project is to generate proofs automatically. It is currently using the Coq proof assistant for proving.

The workflow for easier-proofs is as follows:

- A project is written in an OCaml programming language, defining all the types and function definitions that one wants to use for proving.
- Using the tool namely coq-of-ocaml convert this OCaml program into a Coq program.
- This is the part where one can use easier-proofs to write proofs: write an OCaml program, where it contains all the proofs properties that one wants to prove, and then using the helpers provided from easier-proofs to prove those properties.

‍