Skip to main content
Ryan Orban

Ryan Orban

Subject
6 entries

Formal Verification

Bookmarks

  1. lean-collab: multi-agent theorem proving in Lean 4

    lean-collab applies multi-agent collaboration to Lean 4 theorem proving, using the Ensue Memory Network to coordinate agents across complex mathematical proofs. An unusual intersection of formal verification and multi-agent AI.

  2. The Move Prover: A Practical Guide

    OtterSec's practical guide to the Move Prover — a formal verification tool for the Move smart contract language used on Sui and Aptos. Covers writing specifications that the prover can check, bridging the gap between formal methods theory and blockchain developer practice.

  3. Finding Bugs Automatically in Smart Contracts with Parameterized Invariants

    A 2020 WIP paper from Certora describing a framework of reusable parameterized invariants for automatically finding bugs in smart contracts, with the Certora Prover discovering two real bugs in MakerDAO's Multi-Collateral Dai. The core insight is that the hardest problem in formal verification is specification, and smart contracts are unusually amenable to shared invariants — enabling a community network effect.

  4. Using the Kani Rust Verifier on a Firecracker Example

    Kani is AWS's Rust model checker — a formal verification tool that proves correctness properties of Rust code by exhaustively exploring execution paths. This post shows it applied to Firecracker, AWS's microVM hypervisor, demonstrating industrial-scale use of formal methods.

  5. Formal Verification of an OS Kernel

  6. Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts

    Clockwork Finance Framework (CFF) is a formal verification system for reasoning about economic security in DeFi smart contracts, introducing 'extractable value' (EV) as a rigorous notion. Applied to Uniswap, Sushiswap, and MakerDAO, it automatically discovers $56M/month in MEV-like opportunities.

All bookmarks