
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.

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 Petar Maksimović
August 19th, 2024
Runtime Verification Audits Band Protocol’s Rust Implementation of the Band StandardReference Soroban Smart Contract
by Runtime Verification
March 29th, 2024
Runtime Verification audits MultiversX’s Multi Asynchronous Calls
by Runtime Verification
January 15th, 2024
Runtime Verification audits Zivoe’s Core and Locker Contracts
by Runtime Verification
October 17th, 2023
Runtime Verification conducts a design audit on Zorp’s Eden zkVM
by Runtime Verification
July 31st, 2023Runtime Verification audits Ojo’s Node, Price Feeder and Smart Contract
by Runtime Verification
June 14th, 2023
How audits can optimize code base: Term Finance “clearing price” algorithm
by Runtime Verification & Term Labs
May 9th, 2023
Runtime Verification audits Gyroscope Protocol’s Mathematical Model Implementation
by Runtime Verification
March 29th, 2023
Runtime Verification Audits World Mobile EarthNode NFT Claiming Contract
by Runtime Verification
February 15th, 2023
Runtime Verification audits QuipuSwap Stableswap DEX Factory Mode
by Runtime Verification
September 28th, 2022
Runtime Verification audits Hone’s Liquid Staking protocol
by Runtime Verification
September 1st, 2022

Runtime Verification audits Pact’s Stableswap AMM smart contract
by Runtime Verification
August 23rd, 2022
Runtime Verification audits Blockswap’s Stakehouse code changes
by Runtime Verification
August 4th, 2022

Runtime Verification audits EXA Finance’s Baskets smart contract
by Runtime Verification
May 31st, 2022

Runtime Verification audits QuipuSwap's token-to-token distributed exchange
by Runtime Verification
February 11th, 2022
Runtime Verification audits Yieldly's Multi-token Staking Pool
by Runtime Verification
February 3rd, 2022

Runtime Verification audits Element’s Finance Governance Protocol
by Runtime Verification
November 4th, 2021
Runtime Verification audits the Rewards Contracts of Algorand's Community Governance
by Runtime Verification
October 11th, 2021
Runtime Verification audits XET token and its deployment script
by Runtime Verification
July 19th, 2021