1. Homepage
  2. > Careers >
  3. Verification of OCaml code using the F* language

Verification of OCaml code using the F* language





Nomadic 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.

Apply now

Send us your application


    Application letter

    By submitting this form, I accept that the information entered will be used as part of my request.