Correctness Is Not Optional

This article aims to provide context to formal verification, its different approaches, and why it can provide ultimate assurance of code correctness. Throughout the article, we provide insights into the field of formal verification and some of its components rather than explain how to use a specific tool. These insights should make it clearer to the newcomer to the field why we can claim mathematical rigorousness when we perform formal verification.

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.

Recently you may have heard about our new tool Kontrol, but are still uncertain about what it is or how it might benefit your project’s security. This blog post addresses those concerns by explaining the blockchain security lifecycle, how it differs from traditional software security, and the role that Kontrol plays in ensuring that your application is as secure as possible.

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 and Certora partnered to compare and evaluate a set of testing tools for DeFi applications. In Part 1 of this blog post, we introduced the testing tools. In Part 2, we focus on the bug-detection capabilities of these tools. Specifically, we evaluate and compare them against each other by using mutation testing using Gambit.

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

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.

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.

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.

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.

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