Raoul Schaffranek

Formal Verification for Dummies, Episode 4: Scaling

Using a solidity debugger to explore time and space

By Raoul Schaffranek

Posted on November 22, 2024

It’s been a while since my last post in this series. In the meantime, I’ve published two in-depth technical articles on verifying loop invariants for Runtime Verification. Read them here: Part 1 and Part 2 [Read More]

Tags:

DeFi Security Summit - Solidity under the hood

Using Simbolik to understand compiler internals

By Raoul Schaffranek

Posted on November 8, 2024

Inside the Solidity Compiler: A Peek Into Boilerplate Code & Variable Allocation [Read More]

Tags:

Formal Verification for Dummies, Episode 3: Proofs

Using a solidity debugger to explore time and space

By Raoul Schaffranek

Posted on September 20, 2024

In software development, achieving total confidence in code might sound like an unreachable goal. However, in formal verification, we aim to get as close to certainty as possible using proofs. These aren’t just any hand-wavy arguments—they’re mathematical demonstrations that a program behaves exactly as specified. But don’t worry, I’ll explain... [Read More]

Tags:

Formal Verification for Dummies, Episode 2: Invariants

Using a solidity debugger to explore time and space

By Raoul Schaffranek

Posted on September 12, 2024

Hello again! Today, we’re tackling a super important concept in software testing and formal verification: invariants. If you’ve worked in the Ethereum ecosystem, you’ve probably heard people throw this term around as a catch-all for software requirements, but what does it really mean? In this episode, we’re breaking down the... [Read More]

Tags:

Formal Verification for Dummies, Episode 1: Specifications

Using a solidity debugger to explore time and space

By Raoul Schaffranek

Posted on September 6, 2024

Hey everyone! Welcome to the first episode of my new series, “Formal Verification for Dummies.” My goal here is to explain complicated topics in simple terms to help others and improve my ability to break things down. I’m not sure how many episodes I’ll do or how often I’ll post—this... [Read More]

Tags:

SecureFi - Formal Verification Panel

with Kostas Ferles, Mooly Sagiv, Alexander Hicks and Julian Sutherland

By Raoul Schaffranek

Posted on July 8, 2024

Breaking Down Barriers: Formal Verification in the Blockchain Space [Read More]

Tags:

Web3 Security Summit - Fuzzing vs. Formal Verification Panel

TL;DR: Do both

By Raoul Schaffranek

Posted on June 7, 2024

Formal Verification vs Fuzzing: Key Takeaways from the Panel [Read More]

Tags:

EthBelgrade - Debugging meets Formal Methods

Smart contract debugging and formal verification

By Raoul Schaffranek

Posted on June 5, 2024

Demystifying Formal Verification: Tools and Techniques for Smarter Smart Contract Development [Read More]

Tags:

EthCluj - Formal Verification and Symbolic Execution

How to increase smart contract security

By Raoul Schaffranek

Posted on May 6, 2024

Elevating Smart Contract Security with Symbolic Execution and Formal Verification [Read More]

Tags:

EthBucharest - Using a solidity debugger to explore time and space

About time

By Raoul Schaffranek

Posted on March 30, 2024

Exploring the Future of Smart Contract Debugging with Symbolic Execution [Read More]

Tags:

TrustX - The Symbolic Solidity Debugger

Lowering the entry barrier to symbolic execution

By Raoul Schaffranek

Posted on December 7, 2023

On November 14th, 2023, I had the incredible opportunity to present at the TrustX conference in Istanbul! My topic, “The Symbolic Solidity Debugger,” focuses on making symbolic execution more accessible to everyone. I’m so grateful for the chance to share this innovative tool and connect with so many passionate individuals.... [Read More]

Tags:

EVMSummit - Debugging and symbolic execution of EVM bytecode

Reflecting on an Incredible Hour at EVMSummit

By Raoul Schaffranek

Posted on December 1, 2023

I recently had the honor of leading a 1-hour workshop at the inaugural EVMSummit in Istanbul, focusing on the EVM low-level debugging capabilities of the Symbolic Solidity debugger. It was a deep dive into the intricacies of EVM and how our tool can effectively tackle complex debugging challenges. [Read More]

Tags:

DevCon Bogota - Tackling Rounding Errors with Precision Analysis

A Leap Forward in Smart Contract Precision and Security

By Raoul Schaffranek

Posted on October 20, 2022

Thrilled to share insights from my recent presentation at DevCon Bogota! Titled “Tackling Rounding Errors with Precision Analysis”, the talk highlighted a crucial aspect of smart contract security: the impact of rounding in the wrong direction. [Read More]

Tags: