Runtime Verification

Over the last 6 weeks, Runtime Verification and Term Finance have worked together to formally verify a series of properties that play a key role in the Term Finance’s Tokenized Strategy Protocol.

Term.png

Term Labs

Kontrol and Term Finance: Formal Verification Success Story Working with Bounded Loops

Raoul Schaffranek

Explore how to leverage Simbolik for streamlined Solidity debugging. Learn to automate deployments, simulate user interactions, and create reusable debugging scenarios—all within Solidity.

simbolik-screenshot.png

 Using Simbolik for Solidity Debugging

This blog post continues our journey into formal verification of loops in Solidity and EVM smart contracts. It introduces loop invariants, a challenging but essential technique for reasoning about unbounded loops. We explore natural induction, apply pen-and-paper methods, and then leverage Kontrol to formally prove the equivalence of two Solidity functions, diving deep into EVM bytecode and formal verification tools.

DALL·E 2024-09-25 17.50.48 - A futuristic rollercoaster with multiple loopings, representing symbolic execution and bounded loop unrolling. The rollercoaster track is set against .webp

Formally Verifying Loops: Part 2

Explore the challenges of formal verification in Solidity and EVM smart contracts. Learn about the path explosion problem, bounded loop unrolling, and how tools like Certora Prover, Halmos, hevm, and Kontrol approach verifying loops in smart contracts.

Formally Verifying Loops: Part 1

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

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? 

David Kretzmer

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

foundry_v1.png

Using Foundry to Explore Upgradeable Contracts (Part 1)

Adam Fiedler

warning-code-explosive.png

Warning: Code Can Be Explosive

foundry.png

Foundry: Gen 2 of Ethereum Tooling

algorand-annoucement-2.png

Algorand

Runtime Verification becomes Algorand Foundation’s security partner

staking-banner.png

Security Risks for Staking Providers

cosmosbanner.png

Cosmos

Cosmos modules documentation

rv-and-tezos.png

Tezos

K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)

K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)

Formal Verification Framework for Michelson

Rikard Hjort

rv-and-gitcoin.png

Gitcoin

Ethereum

KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0

rv-2.png

Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements

rv-1.png

Formal Verification 101 for Blockchain Systems and Smart Contracts

Daejun Park

rv-and-eth-3.png

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

Yi Zhang

example-property.png

The RV Bounded Model Checker - A lightweight semantics-based tool

How Formal Verification Could Help to Prevent Gridlock Bug

rv-and-eth.png

Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

Patrick MacKay

rv-offices.jpg

Runtime Verification goes multinational by opening Bucharest based subsidiary

Denis Bogdănaș

k-overview.png

ERC777-K: Formal Executable Specification of ERC777

Brian Marick

specification-for-k-with-hints.png

Formal Verification of ERC20 Contracts

compiled-1.png

Symbolic execution and smart contracts

verification-start.png

How Formal Verification of Smart Contracts Works

We Love Formal Methods

Categories