Welcome to the Runtime Verification blog

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

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.

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.