PositionNomadic Labs is looking for a Verification of OCaml code using the F* language intern.
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* (https://www.fstar-lang.org/) is a general-purpose functional programming language with effects aimed at program verification.
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.
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.
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.
➡️ If you don’t meet all the criteria above, but think you can still be an asset to us, please consider applying.