Verification of Tezos smart contracts with K-Michelson

Published: Nov. 11, 2022, 5 a.m.

b'

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.

'