Verification of OCaml code using the F* language

Tutors : Marco Stronati, Germán Delbianco, Victor Dumitrescu

The Tezos blockchain is a complex piece of OCaml software handling large amounts of valuable assets. Formal verification of software is practical today for a large class of cases, particularly for functional languages. F*1 is a general-purpose functional programming language with effects aimed at program verification.

Internship goals

The goal of this internship is twofold: verify parts of the Tezos codebase using the F* language and improve the tooling used for code verification.

Outline

The properties we are interested in verifying are mostly local, functional properties of data structures (Merkle trees, bounded queues, key-value store, simple state machines).

F* extracts by default to OCaml. However there are a number of aspects of this extraction that can be improved. In particular:

  • improve the readability of the extracted code
  • simplify the use of OCaml's libraries to replace F* libraries without compromising the verified properties
  • developing a F* stdlib for OCaml verification and in particular for Tezos' specific needs.

Profile

The intern should have a good background in Ocaml or Haskell and basic knowledge of software verification. Experience with F*, Coq and other similar theorem proving tools is a plus. The intern should be able to work independently, clearly present their work and propose solutions to the different problems they will encounter.