KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0

The Gitcoin Grant
We launched a Gitcoin Grant to help us build KWasm and KEwasm, executable semantics and formal verification tools for Ethereum 2.0, written in the K framework.

K tools blur the line between specification and implementation. The code is human-readable and a great reference for understanding Wasm and Ewasm, but it also generates a correct-by-construction interpreter.

We want Ewasm to have a specification that you can run your smart-contract with. We have a prototype implementation of Ewasm that we have began using to verify an Ewasm contract with, which we are blogging about.

It is still early days, and right now we want to ramp up and make the prover more powerful, and the tools more accessible for early adopters. In the next three months we want to get KWasm battle-ready. That includes:

• Verifying a prototype smart contract.
• Doing some major refactoring for readability and speed.
• Making educational material in the form of blog posts and webcasts on how to formally verify contracts.

If you think this work is important, you can support us through the Gitcoin Grant, or contact us directly.

Why are we qualified to do this?
We are the formal verification specialists behind KEVM which we used to verify Uniswap, DAI, and the Ethereum 2.0 deposit contract, to name a few.

In collaboration with dlab we’ve written about the work we’ve done so far in verifying using KWasm. The posts cover these specific topics:

• Introducing KWasm, and an intro to symbolic execution
• An intro to Formal Verification using WebAssembly (Wasm)
• Verifying a more complex Wasm function
• Verifying Ethereum-flavored Wasm (Ewasm) Code

In addition to our experience with blockchain projects we have more than a decade of academic track record.

People
The current KWasm team consists of three people:
Rikard Hjort — KWasm lead based in Berlin. Working on speeding up automatic verification, increasing prover capabilities and writing.
Everett Hildenbrandt — Formal modeling engineer in Urbana, Illinois. One of the product owners at Runtime Verification, and the engineer behind KEVM.
Stephen Skeirik — Formal verification engineer in Urbana, Illinois. Interested in the semantics of blockchain systems and bringing formal verification to the masses.