# KWasm: Executable (E)Wasm Semantics for Verification and Profit by Rikard Hjort (Devcon5)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 04:28
- Topics: blockchain, smart contracts, distributed ledger, ethereum, Science & Technology
- Watch: https://streameth.org/watch/yt-0RGA-F9P2w8
- YouTube: https://www.youtube.com/watch?v=0RGA-F9P2w8

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/5/kwasm-executable-ewasm-semantics-for-verificaton-and-profit

KWasm is a project for specifying Wasm in the K framework, much like the EVM was specified with KEVM. KEVM has been used extensively for verifying smart contracts, and as Ethereum transitions to Wasm, it's time to get ready to verify Ewasm contracts.
With KWasm complete, the new focus is embedding it into KEwasm and other blockchain execution interfaces. This talk is a quick introduction to the power of K, our roadmap and how you can use KWasm to start verifying Wasm code.

Speaker(s): Rikard Hjort
Skill level: intermediate
Track: Developer Infrastructure
Keywords: technical

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

[Applause] hey guys undercard one of my key lesson I want to talk about the challenges that we face from building a virtual machine for watch hands we want to run smart contracts a lot you know we want to have a bunch of conference security tools want to be able to audit them one who's that champion all checking for verification and testing and so on usually these are the December tools and we also want to have like consensus what we're building what is the exact behavior of this virtual machine someone held like a trusted runtime when deaf adults mutations or implementers know what you're building you wanted to be perfectly on a big ewis we just want to make sure we can avoid a consensus buttons and again these are all things that people tend to work on separately someone's writing the documentation someone is formalizing maybe my elevator as well so I want to pitch another approach which is would be applied in the cane framework which is this idea that you can kill efforts with case notes basically the idea is that you specify your language once and you drive the tools that might sound like magic but it's only what you're doing with the parser you're not saying that the write a parser it seemed at the time you're probably writing a grammar and the tool is going to generate of horses we we take that same approach with languages to the next level where you specify your language in a formal assume mathematically we could think of it as Matthew to get its programming and from there we generate parses interpreters program verifiers we're working on a bunch of tools like knowledge areas it's on but the idea is like you specify your line is once and then you get a little I'd argue that its ambitious let's derive all the tools from one specification but it's also realistic right never education this and we're doing for quite a few years I'd say he's pretty successful with this so it's not it's not paperwork it's ambitious but it's realistic so one example you might have heard of this KTM it's a formal specification of the EBM in the K framework it's one more like the yellow paper it's not the exact same for Melissa but still it's executable so if you could actually execute the elevator so you can run it as I know it basically and it reads like code with a lot of documentation because we've opted for a literate programming style where you have bunch of documentation and then the floor was all nice tools we generate through this this pituitary console Firefly which is sort of a travel education to build a lot a bunch of dev tools quite a truffle we generate dog that the jello paper is some argue of easier formal specification to read than the yellow paper we do verifications a bunch of every smart contracts ever build immortal self a fault line and I'm working on K wasn't which is just a formalization of pipe assembly in the case remote right now it's most respect of cura webassembly very similar to the officials back which is nice because they work Joe they chose the same formalism as we've been using parallel so it's a testament it's a new form of civil as Kolbe writing rewriting logic or rewriting this it's these tiny betting's we have a prototype embedding for you awesome even though by the state with building prototypes we're working with the polka dot and substrate to wrap up our verification abilities to do for more education on web accessibility and because k so awesome most EDM tools KTM tools will come you awesome tools okay some massaging but the idea is like we're doing blossom now and when you want some kicks in or everything to go and if it doesn't kick in where we just do any other - I mean work and that's what we're doing some sweet there's this photographic you want token after [Applause]