Smart Contract Correctness Proofs
Using the K framework, Runtime Verification can prove correctness of contracts compiled for either the Ethereum or Cardano virtual machines.
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.
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.
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
|Jan 20 2020||End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract|
|Dec 12 2019||K vs. Coq as Language Verification Frameworks (Part 3 of 3)|
|Dec 12 2019||K vs. Coq as Language Verification Frameworks (Part 2 of 3)|
|Dec 12 2019||K vs. Coq as Language Verification Frameworks (Part 1 of 3)|