#Coq language verification#

Some recent Coq-based developments (not necessarily for language-based verification) at Runtime Verification include modeling of the Algorand protocol and verifying its safety, and modeling and verifying Ethereum’s finality mechanism in Casper. K and Coq at Runtime Verificationīoth Coq and K are very capable as language verification frameworks and we at Runtime Verification have been using them regularly to provide our formal modeling and verification services.Įxamples of recent K-based developments include semantics of the Ethereum Virtual Machine KEVM and the generated interpreter and deductive verifier bundled in the Firefly toolset, a complete definition of a blockchain language IELE, a concrete model of Ethereum 2.0 Beacon Chain specification, and KWasm: a formal executable semantics of Web Assembly, among others. We focus here on a particular class of applications, which is verifying programs written in some language, and illustrate differences between them through this lens.

Indeed, the two frameworks are very different and have been developed over the years with different philosophies, objectives and design goals in mind, targeting different analysis and verification methods. This post series is not meant to draw a foundational or detailed comparison of K and Coq. Before we continue, we’d like to note that we have extensive experience with Coq, both as users and as library/framework developers. We hope to convey to the reader why we believe K is more suitable in this context. 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. 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. 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.

Coq language