About Runtime Verification logoWe Love Formal Methods

Runtime Verification website hero

Welcome to the Runtime Verification blog. We have been working in the web3 security space since 2018 and we love to share what we have learned. Our blog posts are a great way to learn about our audits and formal verification engagements with web3 protocols for readers that may find the audit reports too long or technical.

Our authors write about progress on our tooling - ERCx, Kontrol and Simbolik, all of which are designed and maintain with the goal of helping developers and users interact with blockchains more securely. Dive in and learn with us, and if you have any questions contact us.

Formally Verifying Loops: Part 1
Formally Verifying Loops: Part 1
by Raoul Schaffranek
September 26th, 2024
Kontrol 101
Kontrol 101
by Yale Vinson
March 28th, 2024
From 0 to K Tutorial
From 0 to K Tutorial
by Runtime Verification
July 23rd, 2021
A Subtle Rust Bug
A Subtle Rust Bug
by Dwight Guth
June 26th, 2019
Formal Verification of ERC20 Contracts
Formal Verification of ERC20 Contracts
by Brian Marick
August 15th, 2018
K Framework - An Overview
K Framework - An Overview
by Grigore Roșu
March 25th, 2018
RV-Match now supports inline assembly
RV-Match now supports inline assembly
by Dwight Guth
September 19th, 2017