Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

Ethereum 2.0 is coming. And rest assured, it will be formally specified and verified!

Ethereum 2.0 is a new sharded PoS protocol that, at its early stage (called Phase 0), lives in parallel with the existing PoW chain (called Eth1 chain). While the Eth1 chain is powered by miners, the new PoS chain (called Beacon chain) will be driven by validators.

Continue reading

Code smell: Boolean blindness

At Runtime Verification, we are using Haskell to develop the next generation of formal verification tools based on the K Framework. This article describes how we use algebraic data types to write expressive Haskell code.

Bool represents a single bit of information:

data Bool = False | True

The popular term “boolean blindness” refers to the information lost by functions that operate on Bool when richer structures are available. Erasing such structure can give code a bad smell. Using more structure can produce interfaces that are easier to document, use, decompose, and generalize.

Continue reading

Runtime Verification goes multinational by opening Bucharest based subsidiary

Earlier this Fall, Runtime Verification opened a subsidiary in Bucharest, Romania. The new company, Runtime Verification SRL, is located in the heart of the capital city and already staffed by seven persons. The operation’s focus will be two-fold; support the development of the new K in Haskell, and deliver smart contract verification audits for clients building products and services for the Ethereum community and beyond. The founding team consists of Traian Serbanuta (co-inventor of the K-framework), Virgil Serbanuta, Denis Bogdanas, Vladimir Ciobanu, Denisa Diaconescu, Ana Pantilie, and Andrei Vacaru.

Continue reading

ERC777-K: Formal Executable Specification of ERC777

Denis Bogdanas and Daejun Park


The ERC777 standard is a new token standard, designed to be an alternative to the ERC20 standard, improving usability by giving account holders more control over token transactions, while keeping backward compatibility with ERC20. It defines an "operator" who can be thought of as a (trusted) third party to whom an infinite amount of "allowances" is approved to spend on behalf of the token owner. It also introduces the concept of a "hook", a callback function that is triggered when an operator performs a token transfer. The hook can either accept or reject the token transfer, allowing the token holders to have a finer-grained control of delegating the token transfer to operators. This hook can be also used to notify the token holders that they have received tokens, which is an important feature missed in ERC20.

Continue reading

Formal verification of ERC-20 contracts

Brian Marick and Daejun Park

Runtime Verification Inc provides Formal Smart Contract Verification services.

The previous post explained the overall process of formally verifying a smart contract. It wasn't enough, though, to let you imagine what you'd work with as you did the work. This post expands on the previous one using the recent experience of one of us (Park), who verified several implementations of the ERC-20 standard written to run on the Ethereum Virtual Machine (EVM).

Continue reading

How Formal Verification of Smart Contracts Works

Brian Marick and Daejun Park

Runtime Verification Inc provides Formal Smart Contract Verification services.

In this post, we'll describe – in general terms – the process of verifying a smart contract. Later posts in this series will provide more detail, contrast verification to other automated ways of increasing assurance, and cover other topics.

The pieces that matter for testing

Let's look at what any sort of verification has to work with, starting here:

The solidity compiler converts a smart contract into bytecodes

A smart contract is written in a programming language (commonly Solidity) and then translated into bytecodes. Once a smart contract is reduced to bytecodes, it can be deployed on the blockchain as a contract account at some address. An address is a huge number (for reasons irrelevant to this post.)

Continue reading

K Framework – An Overview

Why K

Unlike natural language, which allows interpretation and miscommunication, programming languages are meant to tell computers precisely what to do. Without a rigorous definition of a programming language that unambiguously says what each program does, also called a formal semantics, it is impossible to guarantee reliable, safe or secure operation of computing systems. K is a framework that allows you to define, or implement, the formal semantics of your programming language in an intuitive and modular way. Once you do that, K offers you a suite of tools for your language, including both an executable model and a program verifier.

Why Formal Semantics

Formal semantics of programming languages is a very old field of study, started long before many of us were born, in late 60's (Floyd-Hoare, or axiomatic semantics) to 70's (Scott-Strachey, or denotational semantics) and 80's (various types of operational semantics).

Unfortunately, formal semantics have a negative connotation among practitioners, who think that formal semantics of real programming languages are hard to define, difficult to understand, and ultimately useless. This is partly fueled by the fact that most formal semantics require a solid mathematical background to be understood and even more math to be defined, use cryptic notations that make little sense to non-logicians, such as backwards A and E symbols and a variety of Greek letters, and in the end sell themselves as "helping you better understand your language" and nothing else. Continue reading

Runtime Verification seeking experienced C and C++ engineers

Runtime Verification, Inc., (RV) wants to add a Senior Software Engineer to its team that makes verification tools for C and C++ programs.

RV is a growing startup whose software tools help developers make safe, reliable software that runs on automobiles, airplanes, spacecraft, and the blockchain. RV’s verification technology is state-of-the-art, and the company employs leading experts in software engineering and verification.

RV offers great benefits, and its offices have the best views in downtown Urbana.

In the role of Senior Software Engineer, prior experience writing, testing, and debugging multithreaded C or C++ programs is essential. Familiarity with assembly language, operating system internals, embedded systems, or real-time operating systems is highly desirable.

Experience with test-driven development, Java, compiler implementation (especially using LLVM), functional programming, or formal methods is a plus.

In addition to being technically astute, a successful Senior Software Engineer at RV has to be a considerate teammate with good communication skills, and an eager learner with a demonstrable ability to solve problems.

To apply to this position, email a cover letter and résumé to contact (at) (our domain) (dot) com. Use the words “Careers” and “Senior Software Engineer” in the subject.

IELE: A New Virtual Machine for the Blockchain

IELE and K Team
Runtime Verification (RV) is proud to release their first version of IELE, a new virtual machine for the blockchain.

IELE Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV president/CEO and UIUC professor; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV).

Continue reading