Posts by Raoul Schaffranek
Introducing the Simbolik Contributor Program
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Simbolik Expands into a Full Security Toolkit for Solidity Engineers
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Using Simbolik for Solidity Debugging
Explore how to leverage Simbolik for streamlined Solidity debugging. Learn to automate deployments, simulate user interactions, and create reusable debugging scenarios—all within Solidity.
Formally Verifying Loops: Part 2
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.
Formally Verifying Loops: Part 1
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.
Runtime Verification Hosts EthCluj Workshop on Formal Methods
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.
