K framework for smart contract execution

Charles Hoskinson talking about A Third Generation Smart Contract system introduced us to K framework for formal verification of programming languages. This intro took us to Grigore Rosu who started K in 2003 at UIUC. kframework.org

YOUTUBE eSaIKHQOo4c K-Framework

I had chatted with Norm Hardy, whom Mark S Miller recognizes for teaching him object capabilities-based computer security about how to do formal language verification w/o making certain headway. Charles Hoskinson is betting on the K framework for smart contracts verification in Cardano