PositionNomadic Labs is looking for an Improve our Formal Verification Framework intern.
Tutors: Zaynah Dargaye, Thomas Letan, Boubacar Sall.
The Tezos blockchain places a premium on the quality of its implementation. Formal verification is a natural way 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. These efforts include:
- Formal specification: component specification designs with proof in mind.
- Proof of correctness of the entire code base: it implements a blockchain.
- Code correction: each component of the code behaves as expected.
- Extending and improving the tools used.
Our tools of choice are Coq, FreeSpec, and property-based testing.
If you want to participate in these efforts, either through its implementation on one of our critical components or if you want to participate in the design and implementation of formal tools in an industrial setting, we have a set of topics to offer.
The successful applicant will be in charge of:
- Documenting the pertinent state-of-the-art for the topic.
- Describing, in a rigorous manner, the methodologies and tools that she(he) wants to explore.
- Implementing them on a realistic use case.
To tackle this subject, training in formal methods and program specification is essential. Familiarity with a formal verification tool is welcome, and experience with Coq is a definite plus. Experience with source management such as git is welcome.
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.
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.