Posts by Runtime Verification

Fuzzing is one of the most practical ways to find bugs that unit tests miss, especially in large code bases. At a basic level, a fuzzer repeatedly feeds a series of not-so-randomized inputs into a program with the objective of identifying crashes, failed assertions, unexpected behavior, or broken assumptions. Many modern languages now have good fuzzing support built into or near the standard developer workflow.

A simple bug in the software running inside a pacemaker or an insulin pump is not just a crashed app but it could also put thousands of lives at risk. Software as a Medical Device has raised the stakes of every line of code, and the testing toolkit alone is no longer enough.

A technical analysis of the April 2026 KelpDAO bridge incident, in which $292M was lost despite every audited on-chain component performing exactly as specified, with the actual compromise occurring in the off-chain operational layer that surrounded them.

The most consequential security failures in privacy software rarely come from anyone being careless. They come from properties that held in one place and quietly stopped holding in another.

On April 18, 2026, an attacker drained $292M from KelpDAO's Ethereum escrow in a single transaction. The OFTAdapter contract that released 116,500 rsETH did exactly what it was designed to do. No bug was exploited, no zero-day in LayerZero's on-chain code. The entire on-chain system was, by conventional security standards, clean.

Earlier this week, our team at Runtime Verification participated in Wonderland’s CTF, providing one of the challenges to snatch a piece of the $30,000 prize pool. We want to thank everyone who joined us and worked tirelessly to solve all the challenges (and congrats to the winning teams!).

Over the last 6 weeks, Runtime Verification and Term Finance have worked together to formally verify a series of properties that play a key role in the Term Finance’s Tokenized Strategy Protocol.

Our team is already in Thailand, ready to take over DevCon and the side events organized by different teams in the ecosystem! In this blog, we list all the events where our team will be speaking, how to get in touch with us and meet us, and update you on the latest developments in our tooling.

we’re excited to introduce our latest tool: Komet, a formal verification and fuzzing tool designed specifically for Soroban smart contracts on the Stellar blockchain.

Runtime Verification completed a design review of Lido's dual governance mechanism. This mechanism is the first of its kind, representing a monumental upgrade to the Lido governance model. This collaboration aimed to ensure that the new system, scheduled for testnet release in Q3 2024 and mainnet in Q4 2024, functions as intended and maintains the integrity and security of Lido’s $33 billion in total value locked (as of this writing).

We are pleased to announce our recently completed work with Optimism and Kontrol integration into their CI. Having Kontrol as part of Optimism’s CI produces proof of correctness for critical properties of the code as it evolves.

Runtime Verification is pleased to announce the audit completion of Band Protocol’s rust implementation of the Band Standard Reference Soroban Smart Contract. Band Protocol, built on top of Cosmos, is a cross-chain data oracle platform that aggregates and connects real-world data and APIs to smart contracts.

Runtime Verification is pleased to announce Synonym Finance’s audit completion. Synonym Finance is a cross-chain lending and borrowing protocol powered by the Wormhole cross-chain technology stack and available in Ethereum, Arbitrum, and Optimism chains.

Runtime Verification is pleased to announce MultiversX’s Multi Asynchronous Calls audit completion. MultiversX is a distributed transactional computation protocol that relies on a sharded state architecture and a secure Proof of Stake consensus mechanism.

Runtime Verification is pleased to announce the Zivoe Core and Locker contracts audit completion. Zivoe is a decentralized credit protocol designed to be launched on an Ethereum Virtual Machine compatible blockchain. Its purpose is to disrupt predatory high-interest consumer lending across the globe by supporting more affordable credit solutions to underbanked and underserved communities using cryptocurrency and blockchain payment rails.

Runtime Verification is pleased to announce the completion of the design audit for the Zorp’s Eden zkVM. Eden is a Turing-complete instruction set derived from Nock along with arithmetization techniques to enable its use in zkVMs. The Eden zkVM is part of the Urbit ecosystem and is a zero-knowledge virtual machine used for proving Eden computations within a zk-STARK proof system.

Runtime Verification is pleased to announce the Blockswap dETH Gateway audit completion. The dETH Gateway protocol offers users a bridgeless path to any EVM ecosystem for dETH.

Runtime Verification is pleased to announce the Ojo Node, Price Feeder and Smart Contract audit completion.

Runtime Verification is pleased to announce the completion of the Morpho AAVE V3 audit. Morpho is a lending protocol built on top of AAVE which matches borrowers to lenders peer-to-peer.

Runtime Verification is thrilled to announce the completion of the Proof of Neutrality Network audit. In this post, we give an overview of what the Proof of Neutrality Network is and describe the highlights of its audit.

Gyroscope Protocol's math model implementation audit complete; Ethereum-based, fully-backed stablecoin; diverse reserve; autonomous price bounding. Runtime Verification conducted 6-week review.

Runtime Verification is proud to announce the successful completion of its audit of the World Mobile EarthNode NFT claiming contract. World Mobile is a blockchain-based mobile network aiming to connect people and communities globally. The audit examined the EarthNode NFT claiming smart contract, which manages NFT ownership for node operators, who can earn rewards in the form of the native WMT currency by contributing to the sharing economy. After a comprehensive manual code review, the audit identified some issues and informative findings.

This blog is about Runtime Verification's guidelines for collaborative coding, which are designed to help teams manage their software development process and avoid introducing unneeded friction. It covers topics such as prioritizing work, opening PRs, reviewing PRs, addressing changes, and closing remarks. It also discusses the importance of trust and the use of CI in aiding collaborative coding.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

With K v6 we are modernizing the K Framework. We focused on emphasizing usability and customization in the design to make it easier than ever to generate a set of tools for your programming language environment.