Correctness Is Not Optional

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.

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 is pleased to announce the Ojo Node, Price Feeder and Smart Contract audit completion.

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

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.

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

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