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.
How We Build Formal Verification and Fuzzing Tools: Bridging the Gap Between Developers and Advanced Security Tooling with the K Framework
by Gregory Makodzeba
December 10th, 2024
With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review
by Runtime Verification
September 4th, 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, 2024Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct
by Juan Conejero
April 2nd, 2024
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 completes another successful engagement with PlatON Networks
by Bogdan Stanciu
October 26th, 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, 2020
Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements
by Runtime Verification
March 10th, 2020Runtime Verification enters a protocol verification agreement with PlatON
by Bogdan Stanciu
March 9th, 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
Formally Verifying Algorand: Reinforcing a Chain of Steel (Modeling and Safety)
by Musab Alturki
June 18th, 2019Runtime Verification goes multinational by opening Bucharest based subsidiary
by Patrick MacKay
November 27th, 2018