by Rikard Hjort

Elrond and Runtime Verification started as friends, professional admirers of each other’s organizations. The picture attached to this post shows members of both companies together at DevCon IV in Prague, October 2018. Quickly thereafter, Grigore Rosu, Runtime Verification’s founder and CEO, agreed to become an advisor to Elrond.

by Stephen Skeirik

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. …

by Stephen Skeirik

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…

by Musab A. Alturki

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. …

by Stephen Skeirik

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. …

by Musab A. Alturki, Elaine Li, and Daejun Park

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…

by Rikard Hjort

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…

by Rikard Hjort and Stephen Skeirik

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:

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…

by Stephen Skeirik

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.

by Stephen Skeirik

Blockchain technology coupled with smart contracts offers a tantalizing promise: enabling distributed, trusted, and verifiable computational platforms for applications with rigorous security requirements like finance, secure messaging, and more. Unfortunately, one does not have to look very hard to see that the path to this promise is fraught with danger, e.g., see articles on Mt. Gox, the DAO, this attack on Ethereum classic, and a smart contract bug. While blockchain systems may be sound in theory, in practice, blockchain systems and smart contracts are still highly prone to developer error.

The question proponents of blockchain systems must ask themselves is…

Runtime Verification

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store