Comprehensive. End-to-end. Faithful. Knowing the unknown. We provide cutting-edge formal assurance.
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.
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. Learn more from our GitHub page.
COMPILE & TEST
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.
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.
|Assurance requirements||RV's formal verification||Informal approaches|
|Verifiable properties||Full functional correctness||Only surface-visible properties|
|Correctness guarantees||State-of-the-art in formal verification||Low or none|
|Underlying semantics||Complete formal semantics||Ad-hoc|
|Verification target code||VM bytecode, no need to trust compiler||High-level code, need to trust compiler|