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

Runtime Verification

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

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

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

dexterbanner.png

Dexter

Tezos

Dexter 2’s Formal Verification

Stephen Skeirik

rv-and-tezos.png

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

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

Bogdan Stanciu

rv-and-platon.png

PlatON

Runtime Verification completes another successful engagement with PlatON Networks

Musab Alturki

rv-and-algorand-2.png

Algorand

Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem

Formal Verification Framework for Michelson

Elaine Li

Daejun Park

rv-and-eth-4.png

Ethereum

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

Rikard Hjort

rv-and-gitcoin.png

Gitcoin

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

Runtime Verification enters a protocol verification agreement with PlatON

rv-1.png

Formal Verification 101 for Blockchain Systems and Smart Contracts

rv-and-eth-3.png

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

Brandon Moore

k-vs-coq-2.png

K vs. Coq as Language Verification Frameworks (Part 2 of 3)

k-vs-coq-3.png

K vs. Coq as Language Verification Frameworks (Part 3 of 3)

k-vs-coq.png

K vs. Coq as Language Verification Frameworks (Part 1 of 3)

Denis Bogdănaș

Chris Hathhorn

rv-and-eth-2.png

A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain

Category: verification