Verification of Tezos smart contracts with K-Michelson

Iowa Type Theory Commute

English - November 11, 2022 05:00 - 14 minutes - 9.93 MB - ★★★★★ - 13 ratings
Technology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed

Previous Episode: Start of Season 3: Formal Methods for Blockchain

Next Episode: Mi-Cho-Coq: Michelson formalized and applied, in Coq

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.