How to Reason on Traces between Tezos Nodes

Nomadic Labs is looking for an How to Reason on Traces between Tezos Nodes intern. Tutors: Zaynah Dargaye, Paul Laforgue, Julien Tesson We devote a lot of resources towards the quality of the im

Nomadic Labs is looking for an How to Reason on Traces between Tezos Nodes intern.

Tutors: Zaynah Dargaye, Paul Laforgue, Julien Tesson

We devote a lot of resources towards the quality of the implementation of the Tezos blockchain. Formal verification is a natural part of this effort, helping to ensure that the code behaves as predicted.
The challenge is to reconcile this quality requirement with the imperatives of software that is in perpetual evolution – all the more so because verifying blockchain software in particular 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 designed to provide strong formal guarantees of correctness while integrating smoothly into the Tezos blockchain development workflow.
Our suite for formal verification includes a high-level specification of a Tezos net-work that asserts global invariants to be preserved by each node. From these global invariants, we derive the properties that each node’s component has to satisfy. The Tezos blockchain is a message-passing protocol. Its correctness verification requires reasoning on message traces. By formalizing the Tezos protocol as a set of “correct” messages traces, we can derive: 1. a formal specification against which to verify the OCaml implementation (e.g. “This implementation only produces correct traces”), and 2. a monitoring tool to detect incorrect traces in the network. Finally, reasoning on the message contents enables reasoning on global properties. In Asphalion for example, the reasoning takes place in a distributed lift thanks to a knowledge logic.

Goals

The goal of the internship is to design and develop a logical framework to reason on message traces exchanged during a message-passing protocol.
The successful applicant will be in charge of:
  • gathering the state-of-the-art of formal reasoning on message traces,
  • designing and implementing a well-formed checker,
  • designing and implementing a logical framework to reason on traces.

Requirements

  • Essential: A good grasp of formal methods and program specification.
  • Helpful: Knowledge of distributed systems.
  • Nice to have: Experience of version control tools (e.g. git).

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.