Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#25 Formally Verifying the Tezos Codebase

Formal Land

Nov 21st 2022   |  62 min
0:00
0:00

In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the past developing new features to their source-to-source compiler CoqOfOcaml. In this episode we talk about their work with Tezos and how their techniques are applicable to other codebases as well! For this we talk with Formal Land founder Guillaume Claret and the proof engineers Daniel Hilst and Pierre Vial.

Links