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 

ERCx

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

Runtime Verification

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

Stephen Skeirik

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

Category: Smart Contracts