Support the show, consider donating:
BTC: 1CD83r9EzFinDNWwmRW4ssgCbhsM5bxXwg ( )
BCC: 1M4dvWxjL5N9WniNtatKtxW7RcGV73TQTd ( )
ETH: 0x8cdb49ca5103Ce06717C4daBBFD4857183f50935 ( )
In the past few years, we witnessed the development of multiple smart contract languages – Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools.
We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space.
Topics discussed in this episode:
– Grigore's background with NASA and work on formally verified correct software
– Motivations to develop K framework
– Basic principles behind the operation of K framework
– How K deals with undefined behavior / ambiguities in a language definition
– The intersection of K framework and smart contract technology
– Runtime Verification's collaboration with Cardano
– KEVM and IELE, smart contract virtual machines developed by Runtime Verification
– Broader implications of the K framework for the blockchain industry
Links mentioned in this episode:
– Defining the undefinedness of C – formalisation of C using the K framework:
– IELE – a new virtual machine for the blockchain:
– Runtime verification – Grigore's company:
– K Semantics of the Ethereum Virtual Machine:
– Short video on Grigore's partnership with Cardano:
– An overview of the K framework by Runtime Verification:
– A detailed technical overview of the K semantic framework:
Watch or listen, Epicenter is available wherever you get your podcasts.
Epicenter is hosted by Brian Fabian Crain, Sébastien Couture & Meher Roy.