Daniel Cumming

Runtime Verification is excited to announce the open public alpha of KMIR. KMIR defines the formal operational semantics of the Middle Intermediate Representation (MIR) of Rust in K, giving developers access to the K framework tool suite for MIR programs. 

Non-audit banners (1).png

Runtime Verification

 Introducing KMIR: concrete and symbolic execution of Rust MIR

ERCx

Explore the challenges of developing ERC tokens and delve into Runtime Verification's efforts to provide comprehensive test suites for the most popular ERC standards. Learn about their tools' capabilities, interfaces, and user-friendliness, and see how they compare to other offerings on the market.

erc test suite.png

Towards a Comprehensive ERC Test Suite

Runtime Verification & Certora

Runtime Verification and Certora partnered to analyze a set of tools for detecting bugs in ERC-20 token contracts. In this series of two blog posts, we dive into the tools for detecting bugs in ERC-20 smart contracts.

testing erc20 token.png

Testing ERC-20 Tokens Part 1:  An Arsenal for Bug Detection 

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. 

Audit banners.png

Zivoe

Runtime Verification audits Zivoe’s Core and Locker Contracts 

How confident can we be in the behavior of the contracts? Do they follow the standards as required? With the permissionless nature of blockchains, anyone can write and deploy smart contracts in blockchain ecosystems. Thus, it is important to check that they conform to the standard requirements as stated in their respective ERC standard. 

Non-audit banners.png

Is my ERC-4626 vault token up to the standard? 

Musab Alturki

Yale Vinson

We are thrilled to announce that Runtime Verification has launched a new registered Algorand relay node, contributing to the operation of Algorand’s network

relay node .png

Algorand

Runtime Verification Launches a Registered Algorand Relay Node

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 and Zorp.png

Zorp

Runtime Verification conducts a design audit on Zorp’s Eden zkVM 

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.

Kv6.png

Modernizing K: Enhancing Functionality and Ease of Use

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.

blockswap gateway.png

Blockswap

Runtime Verification audits Blockswap’s dETH Gateway

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.


ercX

Introducing ERCx: <br/>Conformance and Property-checking for ERC Tokens 

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

ojo.png

Runtime Verification audits Ojo’s Node, Price Feeder and Smart Contract

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.

morpho.jpg

Morpho

Runtime Verification audits Morpho’s AAVE V3

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.


PON.png

PON Network

Runtime Verification audits the Proof of Neutrality Network

Runtime Verification & Term Labs

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. 

term labs.jpg

Term Labs

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

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

gyroscope-banner

Gyroscope

Runtime Verification audits Gyroscope Protocol’s Mathematical Model Implementation

Georgy Lukyanov

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

k-framework-formal-verification.png

Runtime Verification Brings Formal Verification to Algorand

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.

world-mobile-audit.png

World Mobile

Runtime Verification Audits World Mobile EarthNode NFT Claiming Contract

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.

github-guidelines-for-collaborative-coding.png

GitHub Guidelines For Collaborative Coding

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

All blog posts