Musab Alturki

Elaine Li

Daejun Park

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

rv-and-eth-4.png

Ethereum

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

rv-and-eth-3.png

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

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

How Formal Verification Could Help to Prevent Gridlock Bug

rv-and-eth.png

Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

k-overview.png

ERC777-K: Formal Executable Specification of ERC777

Brian Marick

specification-for-k-with-hints.png

Formal Verification of ERC20 Contracts

verification-start.png

How Formal Verification of Smart Contracts Works

Author: Daejun Park

Categories