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 covered 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 Episode links: 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 This episode is hosted by Meher Roy and Sunny Aggarwal. Show notes and listening options: epicenter.tv/239

As a society, we have organized as tribes, hierarchies, and markets to accomplish the most impressive of achievements. Human cooperation and collective organization are present at nearly every significant milestone in the history of human civilization. As we move towards an increasingly connected and automated society and economy, there will become a need for decentralized infrastructure which enables companies and markets to make fast decisions at scale. We’re joined by Matan Field, CEO of DAOstack, a new platform that aims to become the operating system for collective intelligence. DAOstack is building a toolset to allow decentralized governance and building self-organizing collectives at scale. Topics covered in this episode: Matan’s background and journey since founding Backfeed What is a DAO and the necessary components to create a functional DAO The role of DAOs in today’s society and over the long-term DAOstack as “WordPress for DAOs” The different layers of DAOstack and their respective roles Holographic Consensus and the governance model of the DAOstack Genesis DAO The purpose of the GEN token and the idea of circular token economies DAOstacks recent crowdsale and upcoming project roadmap Episode links: DAOstack Website DAOstack Introduction Video DAOstack on Medium An Explanation of DAOstack in Fairly Simple Terms Decentralized Governance Matters DAOstack White Paper Epicenter Episode 115 with Matan Field on Backfeed This episode is hosted by Brian Fabian Crain and Sébastien Couture. Show notes and listening options: epicenter.tv/237