Raoul Schaffranek

This blog post continues our journey into formal verification of loops in Solidity and EVM smart contracts. It introduces loop invariants, a challenging but essential technique for reasoning about unbounded loops. We explore natural induction, apply pen-and-paper methods, and then leverage Kontrol to formally prove the equivalence of two Solidity functions, diving deep into EVM bytecode and formal verification tools.

DALL·E 2024-09-25 17.50.48 - A futuristic rollercoaster with multiple loopings, representing symbolic execution and bounded loop unrolling. The rollercoaster track is set against .webp

Formally Verifying Loops: Part 2

Explore the challenges of formal verification in Solidity and EVM smart contracts. Learn about the path explosion problem, bounded loop unrolling, and how tools like Certora Prover, Halmos, hevm, and Kontrol approach verifying loops in smart contracts.

Formally Verifying Loops: Part 1

Juan Conejero

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!


opt3 twitter.png

optimism

External Computation with Kontrol: <br/> Leveraging Foundry Execution for Formal Verification

Petar Maksimović

This is the second post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This installment explains how Kontrol can be used to tackle the complexities caused by dynamically-sized constructs and the challenges associated with the loops that result from them.

opt2 twitter.png

Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs

Runtime Verification

We are pleased to announce our recently completed work with Optimism and Kontrol integration into their CI. Having Kontrol as part of Optimism’s CI produces proof of correctness for critical properties of the code as it evolves.

Opt.kontrol.png

Kontrol Integrated Verification of the Optimism Pausability Mechanism

On April 14th, Andrej Vacaru and Raoul Schaffranek from Runtime Verification were privileged to lead an online workshop hosted by the EthCluj community. We are sincerely grateful for this opportunity, which allowed us to share our passion for innovative software verification tools with an engaged audience.


ethcluj.png

Runtime Verification Hosts EthCluj Workshop on Formal Methods

This article aims to provide context to formal verification, its different approaches, and why it can provide ultimate assurance of code correctness. Throughout the article, we provide insights into the field of formal verification and some of its components rather than explain how to use a specific tool. These insights should make it clearer to the newcomer to the field why we can claim mathematical rigorousness when we perform formal verification.

fv lore.png

Formal Verification Lore <br> Intuitive Intro to Why We Can Prove Programs Correct <br>

Yale Vinson

Palina Tolmach

Recently you may have heard about our new tool Kontrol, but are still uncertain about what it is or how it might benefit your project’s security. This blog post addresses those concerns by explaining the blockchain security lifecycle, how it differs from traditional software security, and the role that Kontrol plays in ensuring that your application is as secure as possible.

We Love Formal Methods

Categories