The Power of Reachability Logic

In a previous blog post, we introduced the K-Michelson project, a project developed by Runtime Verification and funded by a generous grant from the Tezos Foundation. So what is K-Michelson? Simply put, it is a formal verification framework for Michelson smart contracts; see our previous post for details. In this two-part series, we will investigate:

1. What an ideal programming language specification looks like.
2. How this ideal framework powers nextgen program testing.

In the first part of the series, we considered point how the K Framework is an example of point (1) using our K-Michelson tool as a concrete example. …

In a previous post, we introduced the K-Michelson project, a formal verification framework for Michelson smart contracts, and described our overall project goals. In this two-part series, we will investigate:

1. What an ideal programming language specification looks like.
2. How this ideal framework powers nextgen program testing.

In this first part, we limit our focus to question (1). So, what should an ideal programming language specification look like? Several properties come to mind:

• Clarity: it should be unambiguous and straightforward.
• Completeness: It should be self-contained and describe how all possible programs execute.
• Testability: arbitrary programs should be executable against the specification…

We are pleased to announce that Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts. The grant is part of its recently launched 250 Million ALGO Ecosystem Grants Program, a multi-year program that aims to support research and development of the Algorand ecosystem. We are very excited to have the opportunity to collaborate with Algorand in forming the future of Algorand’s smart contract architecture and supporting its growing community of developers. …

Runtime Verification Inc. (RV) is pleased to announce that we are partnering with the Tezos Foundation via the Tezos Ecosystem Grants program to develop a formal verification framework for the Michelson smart contract language! From its inception, the Tezos blockchain was designed with convenience, security, and extensibility in mind. However, unlike the status quo of predecessor technologies like Bitcoin, the true vision of a thriving Tezos ecosystem is more than just a secure digital currency exchange―it is a platform for developing and publishing distributed applications via smart contracts using its smart contract language Michelson. …

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. A key component of Gasper is a finality mechanism that ensures durability of transactions and the continuous operation of the system even under attacks.

We are happy to report the successful completion of another major milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have formally proved key correctness properties of finality in Gasper and used these results to show that…

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…

Welcome to the final installment in the series on formal verification brought to you by Runtime Verification and dlab. If you missed the first three parts, you can find them here:

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

This time around, we’ll be picking up the baton right where we left off as we explore how to verify programs written in Ethereum-flavored Wasm, or Ewasm. In particular, we are going to verify a function for querying the balance of an ERC20-type smart contract.

Ewasm is…

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.