Runtime Verification

We are pleased to announce our recently completed work with Optimism and Kontrol integration into their CI. Having Kontrol as part of Optimism’s CI produces proof of correctness for critical properties of the code as it evolves.

Opt.kontrol.png

optimism

Kontrol Integrated Verification of the Optimism Pausability Mechanism

Bruce Collie

April 2024 saw the release of version 7.0 of the K Framework. Previously, K was focused on the implementation of programming language semantics, and external tool support was required to expand those semantics into production tooling for a language. In K 7.0, we have merged our Python support library for K (Pyk) into the K compiler, making it the primary way for tool developers to interact with K.


k7.png

K 7.0: Improving K for Ecosystem Tool Developers

Raoul Schaffranek

On April 14th, Andrej Vacaru and Raoul Schaffranek from Runtime Verification were privileged to lead an online workshop hosted by the EthCluj community. We are sincerely grateful for this opportunity, which allowed us to share our passion for innovative software verification tools with an engaged audience.


ethcluj.png

Runtime Verification Hosts EthCluj Workshop on Formal Methods

Juan Conejero

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.

fv lore.png

Formal Verification Lore <br> Intuitive Intro to Why We Can Prove Programs Correct <br>

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.


band protocol.png

Band Protocol

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

Yale Vinson

Palina Tolmach

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.

kontrol 101.png

Kontrol 101

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.


synonym.png

Synonym Finance

Runtime Verification audits Synonym Finance

ERCx

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.


testing erc20 part 2.png

Testing ERC-20 Tokens Part 2: Advancing Benchmarking with Mutation Testing

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.


multiversx (1).png

MultiversX

Runtime Verification audits MultiversX’s Multi Asynchronous Calls

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

 Introducing KMIR: concrete and symbolic execution of Rust MIR

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

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 

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

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

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.

All blog posts