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.In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC [University of Illinois at Urbana-Champaign] for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space.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 softwareMotivations to develop K frameworkBasic principles behind the operation of K frameworkHow K deals with undefined behavior / ambiguities in a language definitionThe intersection of K framework and smart contract technologyRuntime Verification's collaboration with CardanoKEVM and IELE, smart contract virtual machines developed by Runtime VerificationBroader 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 frameworkIELE - a new virtual machine for the blockchainRuntime verification - Grigore's companyK Semantics of the Ethereum Virtual MachineShort video on Grigore's partnership with CardanoAn overview of the K framework by Runtime VerificationA detailed technical overview of the K semantic framework Support the show, consider donating: BTC: 1CD83r9EzFinDNWwmRW4ssgCbhsM5bxXwg (https://epicenter.tv/tipbtc)BCC: 1M4dvWxjL5N9WniNtatKtxW7RcGV73TQTd (http://epicenter.tv/tipbch)ETH: 0x8cdb49ca5103Ce06717C4daBBFD4857183f50935 (https://epicenter.tv/tipeth) This episode is also available on :Epicenter.tvYouTubeSouncloud Watch or listen, Epicenter is available wherever you get your podcasts. Epicenter is hosted by Brian Fabian Crain, Sƒbastien Couture & Meher Roy.