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

Verification of OCaml code using the F* language

Paris

Internship

R&D

Position

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.


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.


➡️ 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

    Resume*

    Application letter

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