Welcome to the Runtime Verification blog

Introducing ERCx: Conformance and Property-checking for ERC Tokens

By ERCxJune 15th, 2023

ERCx can be used to check for a contract's security and reusability, but it can also help you develop your own contract that inherits desirable behaviors. In that respect, ERCx favors composability and ensures assumptions are correct.

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 Brings Formal Verification to Algorand

By Runtime VerificationMarch 6th, 2023

We are happy to announce the public beta of KAVM — the formal semantics of the Algorand Virtual Machine built with the K framework!!

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.

GitHub Guidelines For Collaborative Coding

By Runtime VerificationFebruary 10th, 2023

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 Audits AshSwap Protocol

By Runtime VerificationFebruary 1st, 2023

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

Using Foundry to Explore Upgradeable Contracts (Part 1)

By David KretzmerDecember 19th, 2022

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

Runtime Verification Audits Tinyman AMM V2

By Runtime VerificationDecember 12th, 2022

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

Have critical software that has to be right? Let's talk.

Get in touch
10+
Years in formal methods
NASA & Boeing
Early heritage, before blockchain
Trusted
By leading blockchain foundations