Formal Smart Contract Verification

Runtime Verification Inc provides Formal Smart Contract Verification services.

If you are still in the process of deciding between auditing or formally verifying your smart contract, just know that we provide cutting-edge formal assurance. This article explains why and how.

Comprehensive. We specify and verify the full functional correctness of the smart contract. This gives the smart contract owner the strongest possible functional correctness guarantee.

End-to-end. We start with the high-level specification of the smart contract and refine it down to the virtual machine level. The last step is to verify the executable bytecode.

Faithful. We communicate with the smart contract owner to confirm the high-level specification correctly captures the intended functionality. We then prove the soundness of the specification refinements. We will soon generate correctness certificates as formal proof objects to be checked by independent proof checkers.

Knowing the unknown. We detect a compiler’s hidden weaknesses and unexpected behaviors which if left alone could lead to security vulnerabilities and exploits. Simply put, we do not trust compilers, instead we verify the bytecode they generate.

Our Approach

To verify a smart contract, we first formalize it as a mathematical specification. This often requires several rounds of discussions and meetings with the smart contract owner. Opportunities for code improvement are often found at this early stage.

Next we refine the specification to match the target low-level virtual machine (VM), for example the Ethereum VM (EVM) or IELE. We then compile the smart contract from its high-level language (e.g., Solidity, Vyper, Plutus) to VM bytecode (e.g., EVM, IELE). Only then, can we prove the resulting bytecode satisfies the refined specification.

We use the K framework, created in collaboration with UIUC, which includes a correct-by-construction program verifier automatically derived from the formal semantics of the target language or the VM; for example, see KEVM, our formal semantics of EVM, or IELE, a new VM in-development for Cardano. Moving forward, we plan to support EVM-WASM.

Why formal verification

Conventional auditors might suggest changes that improve the code quality or readability, but cannot provide mathematically rigorous artifacts about the code functional correctness. We can provide clear advantages over informal solutions available to you in the market. Lightweight static analysis tools may find some known bug patterns, but may also return high rates of false positives. Ultimately such tools lack the full coverage that specifications tailored to your program can and will provide.

How the process works

There are five main steps in the process:


We formalize the high-level business logic of owner’s smart contract, based on a typically informal specification provided by the owner. We create a precise, customized, and comprehensive specification of the intended functionality of the smart contract, as well as of important properties that it must satisfy.


This high-level specification needs to be confirmed by the owner of the smart contract, possibly after several rounds of discussions and changes, to ensure that it correctly captures the intended behavior of their contract. We have often found bugs in smart contracts at this early stage, before we even started the verification process.


Then we refine the specification all the way down to the VM level, often in multiple steps, to capture the VM-specific details. The role of the final VM-level specification is to ensure that nothing unexpected happens at the bytecode level, that is, that only what was specified in the high-level specification will happen when the bytecode is executed.

Compile & Test

We then compile the smart contract from its high-level code to the resulting VM low-level code, using the same compiler version that will be used to deploy the contract. At this stage we also test the refined specification against the resulting bytecode, using any tests provided by the smart contract owner as well as additional tests that we may develop to increase code and specification coverage.


Finally, we formally verify the compiled VM bytecode of the smart contract against its VM-level specification. Therefore, we do not rely on the correctness of the compiler. To rigorously reason about VM bytecode without missing any VM quirks, we employ the K-framework’s correct-by-construction deductive program verifier, which takes as input a formal semantics of the VM.


Learn more from Runtime Verification Inc. Visit our GitHub page. Send us your questions.

Related story


Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project —

Runtime Verification

Written by

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.



Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project —

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade