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

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

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