Iowa Type Theory Commute

Verification of Tezos smart contracts with K-Michelson

November 10, 2022 Aaron Stump Season 4 Episode 2
Verification of Tezos smart contracts with K-Michelson
Iowa Type Theory Commute
More Info
Iowa Type Theory Commute
Verification of Tezos smart contracts with K-Michelson
Nov 10, 2022 Season 4 Episode 2
Aaron Stump

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.

Show Notes

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.