Watch / KWasm: Executable (E)Wasm semantics for verificaton and profit

KWasm: Executable (E)Wasm semantics for verificaton and profit

  • YouTube
  • IPFS
  • Details

KWasm: Executable (E)Wasm semantics for verificaton and profit

Duration: 00:04:29

Speaker: Rikard Hjort

Type: Breakout

Expertise: intermediate

Event: Devcon 5

Date: Oct 2019

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.
About the speakers


Rikard Hjort

Rikard Hjort is researching formal methods for developing high-assurance smart contracts for blockchains. He worked on formalizing WebAssembly in K, and now uses KWasm to verify smart contracts written in WebAssembly. He has an M.Sc. in Computer Science from the Chalmers University of Technology, Sweden. He was an intern at Google in 2016 and 2017, and studied at the University of Tokyo in 2017-2018 where he combined his research on blockchains with studying coercion-resistant voting protocols.

  • Related