chapter h

In this episode, I talk about two papers from the 3rd International Workshop on Formal Methods for Blockchains, 2021.  Also, I am continuing my request for your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout.  To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science.  Select the Computer Science Development Fund, College of Liberal Arts and Sciences.  Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump.  Sorry it's that complicated.

In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for Certifying
Tezos Smart Contracts", by Bernardo et al.  The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq.  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.  To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science.  Select the Computer Science Development Fund, College of Liberal Arts and Sciences.  Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump.  Sorry it's that complicated.

In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart contract, using their K-Michelson tool, which provides an executable description of the operational semantics of the Michelson language used for smart contracts on the Tezos blockchain.

I start off a new chapter (seventeen!) of the podcast, to talk about formal methods for blockchain systems.  In the next few episodes, we will look at some verification efforts related to the Tezos blockchain.