This is the symbiotic fuzzing+formal verification workflow we use at Runtime Verification 1. Fuzzing with Foundry to quickly catch low-hanging fruits and provide fast feedback loops. 2. Formal Verification with Kontrol to ensure the strongest possible correctness guarantees.

Why is print/PDF still the gold standard for scientific publications? I want to read your paper on my phone, take digital notes, deep-link to your theorems, click through your references, and enjoy interactive charts. But hey, thanks for the list of figures 🤦‍♂️

Great talk by Raoul from Runtime Vеrification — Solidity Debugging meets Formal Methods youtube.com/watch?v=hKO3Ok…

Our team has applied to become Optimism Security Council member. 🔴 Appreciate your support gov.optimism.io/t/security-cou…

GM everyone! ☕ Let's start our day by listening to Raoul from Runtime Vеrification on "Using a solidity debugger to explore time and space" youtu.be/PIS3v9LPPdU

HELP NEEDED! Soldeer Update: We now have around 100 teams using Soldeer in their projects. Some stats: - 75 projects covered - 2,217 revisions (versions) - 88,295 downloads overall Version 0.3.0 is almost ready, just waiting for the Foundry team’s review. Soldeer is trusted

The prize pool for Uniswap Labs 🦄's Cantina 🪐 contest is equivalent to three years of development and maintenance costs for the Truffle debugger (RIP). It makes me wonder if our space is allocating security budgets as efficiently as we could be.

To all computer science professors. This is how your students see your homegrown department website.

This is quite a big moment for me—we’ve finally tagged Kontrol version v1.0. Reflecting on the journey, it’s incredible how much has evolved over the past few years. Prioritizing developer experience and performance proved to be the right call, though some of our design choices

The incompatibility between the IO formats used by Solidity , sourcify.eth , Etherscan , Paradigm 's Foundry, Hardhat , etc., paired with the lack of specs and docs around them, is incredibly frustrating, draining resources and energy. Can we all sit down on a round

Security researchers at work: youtube.com/watch?v=i5oc-7…

Starting in t - 1 minute!

Let's add some color to this tweet for Ethereum specifically. In our ecosystem, "formal verification" is often used as a catch-all term for different techniques to ensure smart contracts work as expected. While these methods can find bugs, they vary in the correctness guarantees

I almost lost my sanity today. The underscore in `request_seq` cost me almost a day of debugging. It's the only name in the debug adapter protocol specification that uses snake_case instead of camelCase.

x.com/i/article/1831…

Since everyone loves Docker, I suspect it's working on everyone else's computer, and I should be happy for you. But today, it's hard for me.

x.com/i/article/1834…

🚨🎉Foundry now supports several Kontrol cheatcodes, making it easier to write fuzzing and symbolic tests that can be analyzed by both tools: github.com/foundry-rs/fou… [1/4]

Sure, it's cool if your program compiles the first try. It's even cooler if your tests pass on the first try. But have you ever experienced the sensation of proving your formal verification claim first try? Me neither