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.
Runtime Verification Audits World Mobile EarthNode NFT Claiming Contract
by Runtime Verification
February 15th, 2023Runtime Verification becomes Algorand Foundation’s security partner
by Runtime Verification
December 9th, 2021
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 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, 2020Formal 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, 2019
Runtime Verification Completes Initial Formal Verification of Ethereum Casper Protocol
by Patrick MacKay
November 27th, 2018
Runtime Verification goes multinational by opening Bucharest based subsidiary
by Patrick MacKay
November 27th, 2018
New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)
by Grigore Roșu
October 25th, 2017
ASE 2001 paper that helped shape the Runtime Verification field got the Most Influential Paper Award
by Grigore Roșu
October 30th, 2016