Quick but Correct: Invariant-powered Property Testing

Tutors: Arvid Jakobsson and Zaynah Dargaye

Tezos is a blockchain developed with a focus on governance and security. It is a highly critical software and so requires a high level of code quality.

To this end, the Tezos code base is written in OCaml, a strongly-typed functional language. In addition, Nomadic Labs applies testing and formal verification.

While testing enables bug finding, it cannot guarantee correctness due to its incompleteness. Efficient formal verification, on the other hand, requires a dedicated workflow that requires time and expertise, as well as a fine knowledge of the code.

Property-based testing1 is a "light-weight" formal method, bridging the two approaches. Property-based tests generalize unit tests: instead of testing one execution path, the test specifies an invariant and verifies it under a large set of randomly generated inputs.

However, the programmer is required to manually specify such properties, while there is a large set of widely applicable and reusable invariant patterns, such as commutativity. Additionally, the programmer must write repetitive "boiler plate" data generators for the input type of tested functions.

Goals

The first goal of this internship is to develop an annotation-based system for specifying invariants of OCaml functions, similar to tags in OCamldoc comments2. Second, to implement a PPX3 preprocessor that transforms the annotations to property-based tests. Finally, to generate data generators.

Challenges

  • Identifying a set of invariant patterns in the Tezos code base.
  • Designing and implementing an annotation-based system to denote invariant patterns.
  • Learning about property-based testing and OCaml code generation.
  • Learning and modifying the code base of Tezos.

Requirements

You should have knowledge of the OCaml programming language and some basic notions in formal verification and testing. Experience with source management tools such as Git is welcome.

Internship Context

You will work at the Nomadic Labs' offices in Paris or Grenoble.

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