Turn complexity into confidence
Runtime Verification designs formal models for high-value application domains, then uses the models to develop domain-specific products and services focused on correctness and security.

Smart Contract Correctness Proofs

Using the K framework, Runtime Verification can prove correctness of contracts compiled for either the Ethereum or Cardano virtual machines.

Prove your contracts


Firefly is a tool for helping Ethereum smart contract developers visualize and discover holes in the existing test-set, and guide them towards full coverage of their contract.

Try it now

Formal Design and Modeling

Formal methods model complex systems as mathematical entities. Models written in the K language are not just descriptive; they are also executable. For example, our model of the C programming language produces a C interpreter. Our models of low-level blockchain languages produced the KEVM and IELE blockchain virtual machines.

The formal model can be used in proofs of correctness. The executable implementation can be extended to produce other tools, such as one that checks whether arithmetic overflow is ever possible.

Design with us

How We Work:
The IELE Virtual Machine

IELE is a virtual machine (VM) that runs blockchain smart contracts. With Cardano funding, Runtime Verification created IELE to be an evolutionary step beyond the Ethereum virtual machine (EVM).

IELE’s formal specification is approximately 5,500 lines of commented K. From that, the K framework generates an executable VM. That means those 5,500 lines of K provide the same value as a VM like the Go version of EVM and its 39-page semi-formal specification.

Explore IELE

Supporters & Contributors

The K Formal Semantics Framework

K lets you design the formal semantics of your programming language in a modular and intuitive way, then uses the semantics to generate a suite of language tools including a parser, execution engine, symbolic execution engine, state-space explorer, and even a program verifier.

Read more

The K Community

The K Team was started in 2003. K has been continuously developed since then, with the center of the community being the FSL research group at the University of Illinois in Urbana-Champaign, USA.

Visit the community