Category: audits

Press archive (to 2021)

With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review

By Runtime VerificationSeptember 4th, 2024

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).

External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification

By Juan ConejeroAugust 28th, 2024

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!

Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs

By Runtime VerificationAugust 19th, 2024

This is the second post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This installment explains how Kontrol can be used to tackle the complexities caused by dynamically-sized constructs and the challenges associated with the loops that result from them.

Runtime Verification Audits Band Protocol’s Rust Implementation of the Band StandardReference Soroban Smart Contract

By Runtime VerificationMarch 29th, 2024

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 audits Synonym Finance

By Runtime VerificationMarch 1st, 2024

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 audits MultiversX’s Multi Asynchronous Calls

By Runtime VerificationJanuary 15th, 2024

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 audits Zivoe’s Core and Locker Contracts

By Runtime VerificationOctober 17th, 2023

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 conducts a design audit on Zorp’s Eden zkVM

By Runtime VerificationJuly 31st, 2023

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 audits Blockswap’s dETH Gateway

By Runtime VerificationJune 28th, 2023

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 audits Ojo’s Node, Price Feeder and Smart Contract

By Runtime VerificationJune 14th, 2023

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

Runtime Verification audits Morpho’s AAVE V3

By Runtime VerificationJune 13th, 2023

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 audits the Proof of Neutrality Network

By Runtime VerificationMay 29th, 2023

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.

How audits can optimize code base: Term Finance “clearing price” algorithm

By Runtime Verification & Term LabsMay 9th, 2023

We are delighted to announce the completion of a successful two-week audit of the Term Finance Protocol. For this engagement, Runtime Verification was tasked with examining a small, critical part of its codebase, with the goal of establishing code correctness, discovering edge-case behavior, and optimizing gas consumption.

Runtime Verification audits Gyroscope Protocol’s Mathematical Model Implementation

By Runtime VerificationMarch 29th, 2023

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 Audits World Mobile EarthNode NFT Claiming Contract

By Runtime VerificationFebruary 15th, 2023

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.