Formal verification of Mina


I am wondering if there is any interest in formal verification of Mina. I have not found resources on the matter yet, although this may be related to the fact that the project is young. In particular, since Mina is written in OCaml like Tezos, some tools developed by the Tezos Foundation could be used for Mina too. As a disclaimer, I am the main contributor to the Coq Tezos of OCaml | Coq Tezos of OCaml project to automatically translate the Tezos kernel to Coq using coq-of-ocaml coq-of-ocaml and write proofs on it. We could probably configure and run coq-of-ocaml on critical parts on Mina too and verify properties on this code. For Tezos, some static analysis tools on OCaml are also being developed, although I know less about these projects.

So are there any plans or interest for formal verification on Mina? What do people think in terms of priorities?

Guillaume Claret

1 Like