Comparing Program Proof Tools for OCaml Programs in an Industrial Setting

Nomadic Labs is looking for a Comparing Program Proof Tools for OCaml Programs in an Industrial Setting intern. Tutors: Zaynah Dargaye, Thomas Letan. The Tezos blockchain places a premium on the

Nomadic Labs is looking for a Comparing Program Proof Tools for OCaml Programs in an Industrial Setting intern.

Tutors: Zaynah Dargaye, Thomas Letan.

The Tezos blockchain places a premium on the quality of its implementation. Formal verification is a natural part of this to ensure that the code behaves as predicted.
The challenge is to meet both this quality requirement and the reality of software in perpetual evolution. Moreover, verifying a blockchain means understanding and being able to reason about a distributed system in an open and potentially hostile environment.
We are building a suite of formal tools to take advantage of the strongest formal guarantees while adapting to the Tezos blockchain development process.
Our suite of tools for formal verification includes a framework for deductive verification in Coq, FreeSpec. Our choice was motivated by our expertise as proof engineers according to the following criteria: coverage of our codebase, the high degree of formal guarantees provided, compatibility with high-level reasoning, usability, maintainability of the tool, and the proof scripts.
We would like to challenge this choice to other existing solutions for program verification through a feedback and comparison document on our criteria.

Goals

The goal of this internship is to drive a comparison between FreeSpec and other pro-gram proof tools for OCaml by experimentations. The witness of thoses experimentation will be a component that is already verified in our framework. The program proof part will be run in the alternative tools. A report on the experimentation will focus on our criteria and provide a comparison and recommendation for improvement.
The successful applicant will be in charge to:
  • select two other program proof tools based on their descriptions or accessible information,
  • perform the verification in both alternatives
  • Write clear feedback experiences

Requirements

For this, a background in formal methods and program specifications is essential. Familiarity with a formal verification tool is welcome. Practical experience develop-ing in OCaml is a definite plus. Experience with source management such as git is welcome.

Internship Context

You will work at the Nomadic Labs’ offices in Paris.
Participating in a large scale open-source project you will have to rapidly learn to use collaborative tools (Git, merge request, issues, gitlab, continuous integration, documentation) and to communicate about your work. The final results might be presented at an international conference or workshop.
You will have a designated advisor at Nomadic Labs and will have to work independently and to propose thoroughly-considered solutions to the different problems you will have to solve. You will be encouraged to seek advice from members of the team.

Intellectual Property

All material produced (essays, documentation, code, etc.) will be released under an open source license (e.g. MIT or CC).

➡️ If you don’t meet all the criteria above, but think you can still be an asset to us, please consider applying.