In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for Certifying
Tezos Smart Contracts", by Bernardo et al.\xa0 The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq.\xa0 This is used to prove a correctness property about a Multisig contract.
I also kindly solicit your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout.\xa0 To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science.\xa0 Select the Computer Science Development Fund, College of Liberal Arts and Sciences.\xa0 Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump.\xa0 Sorry it's that complicated.