Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Verification of Tezos smart contracts with K-Michelson
•
Aaron Stump
•
Season 4
•
Episode 2
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.