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.

Continue reading

Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements

In this second part of our four part series, we will discuss the process of formalizing system requirements and how it fits into the larger context of formal verification for blockchain systems and smart contracts.

Recall that formal verification is all about knowing whether our system implementation (e.g., blockchain system/smart contract), satisfies our system requirements.

Today’s article is about the process of converting our requirements document into an equivalent formal, mathematical requirements specification.

Continue reading

Runtime Verification Enters a Protocol Verification Agreement with PlatON

Runtime Verification is excited to announce a new engagement with PlatON Networks, a privacy protecting new generation of public chain sponsored by LatticeX Foundation (Singapore). PlatON was forked from Ethereum, reborn with a brand new consensus algorithm and PlatON POS (proof of stake). The focus of this engagement is the formal modeling of PlatON’s Concurrent Byzantine Fault Tolerance (CBFT) protocol and verification of two mission critical properties - safety and liveness. The latter will likely be spread out over two different engagement phases.

Continue reading