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

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

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