Internship Goals

1. model a piece of OCaml code in F*, specifying and proving interesting properties that it should satisfy.

2. extract a certified OCaml implementation from the model, with which to replace the original implementation.

3. extract the specification itself from the model, as Property Based Tests for the OCaml code.

We consider this last step very important, as it helps to close the verification gap , i.e. the semantic difference between the verified model and the actual OCaml code.