This is the third and last part of the “K vs. Coq as Language Verification Frameworks” post series. After illustrating how the syntactic structures of a language are defined (Part 1), and how its semantics can be defined and tested (Part 2) in both K and Coq, we now describe how the third step in the verification workflow, which is specifying and verifying correctness properties, can be achieved. We use the same working example SUM and assume all the language definitions of IMP and SUM described in the previous parts.
In Part 1 of this post, we began by generally introducing the steps needed to verify the correctness of programs in a language verification framework, such as K and Coq. We then described how the first step, defining language syntax and program structure, can be accomplished in both K and Coq for our working example program SUM in the language IMP, highlighting the main differences between the two frameworks.
In this second part of the post, we build on the definitions introduced in the previous part and describe how the semantics of the language and testing the semantics, the second step in the process, can be achieved in K and Coq using the same example SUM. Part 3 of the series explains how the third step (specifying and verifying properties) can be done.
Formally verifying programs, like verifying smart contracts in blockchain systems or verifying airplane flight controllers in embedded devices, is a powerful technique for assuring correctness and increasing reliability of systems. In this context, the question of “Why use K as opposed to Coq?” seems to come up quite often when discussing K with colleagues who may not be familiar with K, but have heard about or used Coq before. In this series of posts, we make an attempt at highlighting some of the important ways in which K and Coq differ as formal verification frameworks for languages through a working example. We hope to convey to the reader why we believe K is more suitable in this context. Before we continue, we’d like to note that we have extensive experience with Coq, both as users and as library/framework developers.
With the upcoming major update to version 2.0 (code-named Serenity), Ethereum is transitioning into a sharded, proof-of-stake (PoS) consensus mechanism. It brings better energy-efficiency, security and scalability. The specific PoS protocol of Ethereum 2.0 is known as the Beacon Chain.
We are happy to report the first 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 completed the executable formal model of Beacon Chain in the K Framework. The K specification, along with the technical report describing this work, are both available online.
So what’s the Beacon Chain? How was its model in K developed? Why is this development important?
Runtime Verification, a premium provider of formal verification services announced that it has joined the Enterprise Ethereum Alliance (EEA), the defacto standards organization for enterprise blockchain – one that is backed by the largest developer community in the world and a worldwide member-base.
As a member of the EEA, Runtime Verification will collaborate with industry leaders in pursuit of Ethereum-based enterprise technology best practices, open standards, and open-source reference architectures.
Here at Runtime Verification, we are spending time developing and improving tools for the K Framework. In particular, one of the projects I have been working on is a new execution engine for concrete execution of programs in K semantics, which compiles to LLVM.
Because we compile to LLVM, we are able to make use of code in any programming language that targets LLVM. In particular, we use Rust for the portion of the runtime which handles operations over lists, maps, and sets.
Yesterday I discovered a very subtle bug in our Rust code which was causing our tests to fail. It was affecting the hash algorithm we use for maps and sets, which in turn caused a map lookup operation to fail even though the key it was supposed to look up was in fact in the map.
Earlier this year, Runtime Verification was engaged by Algorand to verify its consensus protocol. We are happy to report that the first part of the effort, namely modeling the protocol and proving its safety theorem, has been successfully completed. Specifically, we have used a proof assistant (Coq) to systematically identify assumptions under which the protocol is mathematically guaranteed to not fork.
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.
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.