Send your Application
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.
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:
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.