Each year we host around half-a-dozen interns (stagiaires), for periods of two to six months. These young men and women are usually studying or have just finished studying for undergraduate or Master’s degrees, and are eager to gain experience in the blockchain industry. Each has a unique story to tell about their individual interest in this technology.

In this blogpost, we will ask three questions of one of our current interns: Antonio Locascio (and a couple of questions of his mentors at Nomadic Labs).

Antonio — so happy to have you with us! We hope you’re having a wonderful and educational period with Nomadic Labs. We’d love to hear a bit about you and your activities chez nous …

Questions for Antonio

1. Please present yourself and your academic background

I graduated last year as a Licentiate (a five-year undergraduate degree) in Computer Science from the Universidad Nacional de Rosario, in Argentina (where I’m from). My main academic interests since my time at university are in the fields of functional programming, programming languages and type systems. For my Licentiate thesis, I worked on a bidirectional type-and-effect system for a core language with algebraic effects, under the supervision of Mauro Jaskelioff and Exequiel Rivas.

Towards the end of my studies, I became quite interested in the field of formal verification, although I didn’t have much first hand experience in it. This was one of the reasons I was so keen on doing this internship, as it was a great opportunity to learn more about this topic while working on real-world problems.

After graduating, I was still undecided on which career path to take regarding whether to continue in academia or go straight to industry. I figured that doing an internship could help me with this decision, and there was hardly a better place to do so than in Nomadic Labs. Here, I would get a taste of what working in an industrial setting is like while still being exposed to, and taking part in, the most recent developments in the academic fields.

2. Tell us more about your internship: main subject, who is your mentor, what you have learned and especially, what surprised you the most within these months?

My mentors for my internship here at Nomadic Labs are Marco Stronati, Germán Delbianco and Victor Dumitrescu. I’ve been working on verifying OCaml code using the F* language. F* is a hybrid verification-oriented programming language. This means that it not only has the expressivity of interactive theorem provers based on dependent types, but thanks to its SMT support it can also automatically prove many properties.

The goal of my internship is to evaluate a verification workflow consisting of three steps. The first one is to model a piece of OCaml code in F*, specifying and proving interesting properties that it should satisfy. When this effort is completed, the next step is to extract a certified OCaml implementation from the model, with which to replace the original implementation. The third step, perhaps the most novel, is to extract the specification itself from the model, as Property Based Tests for the OCaml code. We consider this last step very important, as it helps to close the verification gap, i.e. the semantic difference between the verified model and the actual OCaml code.

Concretely, I’ve first applied this workflow to the implementation of Sapling, a protocol used in Tezos for enabling privacy-preserving transactions. The main verification effort for this initial case study was focused on its storage, which consists of a special type of Merkle tree. After finishing with it, I’ve moved on to the ZK-Rollup project, which proposes a Layer 2 scalability solution with minimal impact on the main chain. Before starting its verification, I’ve been working on a prototype OCaml implementation that is helpful for tinkering with its design. The Rollup’s storage is also a Merkle tree, so the experience from the Sapling model will definitely come in handy for this new verification effort.

I’ve learned a lot during these months: from verification and testing techniques, to code reviewing and good programming practices. All of those things point to what probably surprised me the most for now, which is the importance given to program correctness here at Nomadic Labs. Although it should be expected for a company working on critical code, it was great to see that correctness was emphasized at every step of the pipeline, which is sadly not the case very often.

3. Why did you choose to become a part of the blockchain ecosystem and Nomadic labs? What are your plans after completing this internship?

Although I didn’t really know much about blockchain, the nature of it being an emerging technology with many interesting problems still to be solved compelled me. This field is perfect for verification, as there are plenty of important properties about their implementation that are worth proving. As I explained above, the appeal of Nomadic Labs is its rigorous scientific background, which guarantees an opportunity to learn about interesting new developments and ideas. After my internship, I plan to continue working as a developer on cutting edge projects such as this one.

Questions for Antonio’s Nomadic Labs mentors Marco Stronati and Germán Delbianco:

What is your input to the work of Antonio?

As Antonio’s mentors, our role is to provide guidance based on our combined experience working on the development of the Tezos Economic Protocol, on mechanized software development and verification, and in the toolchain itself. We plant seeds, in the form of suggesting relevant academic literature or related projects; we brainstorm ideas together; we provide feedback on his contributions; and answer his questions. Occasionally, we also warn him of known pitfalls, and of Here be dragons.

That said, we are pleased by the fact that Antonio has hit the ground running on this project, and by the independence he has shown. In order to implement the objectives we had devised together, he not only succeeded in learning how to verify programs in F*, but also he quickly realized how to improve the toolchain so that we could take the most out of this experiment. This makes this work relevant not just to us at Nomadic Labs, or to the Tezos ecosystem at large, but eventually to the F* community as well.

Why is the topic of this internship important?

Making verification techniques scale up to a large industrial, cutting edge, project is a Herculean task. In our case, one of the great hurdles is tightening the verification gap between a mechanization in F*, and the real-world Tezos implementation in OCaml. In a large and complex codebase like ours, there is inevitably a semantic distance between the abstract models we build for the verification of critical components of the Tezos Economic Protocol, such as Sapling or ZK-rollups, and the nitty-gritty of their implementation.

In this project we are indeed interested in reducing this semantic gap, by recovering specifications from the F* mechanization, to validate both the extracted OCaml code and the (different) implementations in the codebase.

Extracting the specification as property-based tests automatically from a mechanized implementation (technically, from dependently-typed signatures) is a (to the best of our knowledge) novel contribution of this internship. Usually, tools like F* (or Coq, or Agda) are designed so that specs and proofs are erased from type signatures, and thus they do not feature in the extracted code — they are lost! Antonio’s solution to recover them is quite elegant, as it relies on two existing F* features — meta-programming and tactics — to extract the definitions and the specs as QCheck tests. Hence, this approach doesn’t require modifying how the extraction mechanism in F* works, but only some tweaking of the Meta-F* framework.

In an ideal world, we would like to have a development cycle which efficiently integrates and interweaves concurrent verification and development efforts. This requires developing common specification styles and languages that can be shared by developers and verifiers¹. This internship provides a plausible approach: by extracting specs from F* and translating them directly to QCheck tests, we can ensure that the specs and definitions in both F* and OCaml — that is both in Proofs and Tests — are two correct reifications of the same concepts, increasing our confidence in the verification process.