We Love Formal Methods
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.
Kontrol and Term Finance: Formal Verification Success Story Working with Bounded Loops
by Runtime Verification
December 2nd, 2024
Introducing Komet: Smart Contract Testing & Verification Tool for Soroban, Created by Runtime Verification
by Runtime Verification
September 19th, 2024How to get started with Komet - Property Testing and Formal Verification for Soroban
by Runtime Verification
September 19th, 2024
External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification
by Juan Conejero
August 28th, 2024
Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs
by Runtime Verification
August 19th, 2024Kontrol Integrated Verification of the Optimism Pausability Mechanism
by Runtime Verification
May 16th, 2024Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct
by Juan Conejero
April 2nd, 2024
Runtime Verification Raises $5.3 Million to Advance Blockchain Security
by Runtime Verification
June 18th, 2021
MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics
by Rikard Hjort
January 5th, 2021
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)
by Runtime Verification
December 11th, 2020K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)
by Runtime Verification
November 2nd, 2020
Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem
by Musab Alturki
July 28th, 2020
KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0
by Rikard Hjort
March 26th, 2020Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements
by Runtime Verification
March 10th, 2020Formal Verification 101 for Blockchain Systems and Smart Contracts
by Runtime Verification
February 18th, 2020End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
by Daejun Park
January 20th, 2020
A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain
by Musab Alturki
October 22nd, 2019
New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)
by Grigore Roșu
October 25th, 2017