Smart Contract Correctness Proofs
Using the K framework, Runtime Verification can prove correctness of contracts compiled for either the Ethereum or Cardano virtual machines.
C/C++ Toolkit
Runtime Verification technology leverages your existing test suite to automatically and accurately detect the rarest, trickiest, and most costly bugs lurking in your code - while avoiding false alarms.
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.
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.
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
