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

the appeal of Nomadic Labs is its rigorous scientific background, which guarantees an opportunity to learn about interesting new developments and ideas

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

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.

1. model a piece of OCaml code in F*, specifying and proving interesting properties that it should satisfy.

2. extract a certified OCaml implementation from the model, with which to replace the original implementation.

3. extract the specification itself from the model, as Property ...