I am pleased to present the coq-of-ocaml project, to translate a subset of OCaml to the Coq proof assistant. The aim is to do formal verification on OCaml programs. The idea is to generate a Coq translation as close as possible to the original code in terms of intent but using the Coq syntax. As a short example, if we take the following OCaml code and run `coq-of-ocaml`

:

```
type 'a tree =
| Leaf of 'a
| Node of 'a tree * 'a tree
let rec sum tree =
match tree with
| Leaf n -> n
| Node (tree1, tree2) -> sum tree1 + sum tree2
```

we get the following Coq file:

```
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.
Arguments Leaf {_}.
Arguments Node {_}.
Fixpoint sum (tree : tree int) : int :=
match tree with
| Leaf n => n
| Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
end.
```

We support the following OCaml features:

- the core of OCaml (functions, let bindings, pattern-matching,…)
- type definitions (records, inductive types, synonyms, mutual types)
- monadic programs
- modules as namespaces
- modules as polymorphic records (signatures, functors, first-class modules)
- multiple-file projects (thanks to Merlin)
- both
`.ml`

and`.mli`

files - existential types (we use impredicative sets option in Coq)

We also have some support for the GADTs, the polymorphic variants, and the extensible types. We are in particular working on having an axiom-free translation of the GADTs to Coq. We do not support:

- side-effects outside of a monad (references, exceptions, …);
- object-oriented programming;
- various combinations of OCaml features for which
`coq-of-ocaml`

should generate a warning.

Our main example and use case is the coq-tezos-of-ocaml project. This contains a translation of most of the economic protocol of the Tezos blockchain (around 30.000 lines of OCaml translated to 40.000 lines of Coq). For example, we verify the comparison functions defined in src/proto_alpha/lib_protocol/script_comparable.ml with src/Proto_alpha/Proofs/Script_comparable.v.

We are looking for the application to other projects too.

We think the best way to use `coq-of-ocaml`

is to continue developing in OCaml and run `coq-of-ocaml`

to keep a synchronized translation in Coq. Having a working Coq translation (as compiling in Coq) forces us to avoid some OCaml constructs. We believe these constructs would probably be hard to verify anyway. Then, on the Coq side, we can verify some important or easy to catch properties. If there is a regression in the OCaml code, re-running `coq-of-ocaml`

should make the proofs break.