#25 Formally Verifying the Tezos Codebase - Formal Land
Type Theory Forall
English - November 21, 2022 16:05 - 1 hour - 53.9 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #24 The History of Isabelle - Lawrence Paulson
Next Episode: #26 Mechanizing Modern Mathematics - Kevin Buzzard
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
Formal Land Website
Formal Land Email: [email protected]
Formal Land Twitter: @LandFooBar
CoqOfOcaml
The DAO hack