[RFC] ROCQ formal proofs for consensus-critical invariants

[TheFrozenFire]

Description

A meaningful fraction of vibehouse's implementation is agentic — diffs are generated, reviewed at a high level, and merged quickly. That workflow trades off the deep per-line scrutiny that normally catches subtle correctness bugs in consensus code. Formal proofs can close that gap mechanically: a proof assistant rejects the diff if a stated invariant no longer holds, regardless of how the change was authored.

The proposal is to add a ROCQ proof layer targeting the consensus-critical components where correctness is hardest to test exhaustively and most expensive to get wrong. The approach: hand-model the Rust semantics in ROCQ, prove soundness and completeness properties against the model, and add integration tests that validate the Rust implementation satisfies the proof assumptions. Axioms are tracked explicitly in a TRUST_ASSUMPTIONS.md.

Prior work

The Ethereum formal verification landscape is worth understanding before starting:

Runtime Verification — Gasper in Coq (2020): beacon-chain-verification. Three key theorems proven at the abstract protocol level: Accountable Safety, Plausible Liveness, and Slashable Bound. These are proven over an abstract validator set model — not tied to any concrete state transition implementation. The planned bridge from this abstract model to the concrete Python pyspec was listed as ongoing and was never completed. This is the most directly reusable prior work for vibehouse since it's already in Coq/ROCQ and covers the core safety properties we care about.

ConsenSys/EF — Dafny beacon chain (TACAS 2022): eth2.0-dafny, paper. Phase 0 only, covers runtime error absence (no array OOB, no integer overflow) and SSZ round-trip correctness. BLS signatures and hash functions are axiomatized. Inactive since ~2021. Nothing for Altair+.

Galois — blst BLS verification (Cryptol + SAW): BLST-Verification. Partial verification of blst assembly routines. Documented gaps: aggregate verification is incomplete, variable-length inputs proven only for specific sizes, elliptic curve group laws are axiomatized.

The common thread: all prior work targets Phase 0 and none of it has been updated for post-Merge forks. Nothing formally addresses ePBS, the fork choice extensions for payload timeliness, or any Gloas-specific logic.

Steps to resolve

What to prove, in priority order:

Tier 1 — Proto-array fork choice — head selection, pruning, and the should_extend_payload logic added for Gloas. Key invariants: the selected head is always a descendant of the justified checkpoint; pruning never removes any block on the canonical chain; should_extend_payload correctly reflects the (is_payload_timely && is_payload_data_available) || ... disjunction. The Runtime Verification Coq proofs provide abstract safety properties we can import as axioms and refine toward the concrete implementation.

• https://github.com/dapplion/vibehouse/blob/55c8282d95b18e9ef85ea39d30ccc7776f1ef892/consensus/proto_array/src/proto_array_fork_choice.rs

Tier 2 — PTC quorum and builder payment arithmetic — the 60% quorum threshold, the builder_pending_payments slot indexing formula (SLOTS_PER_EPOCH + slot % SLOTS_PER_EPOCH), and the payment sweep logic. The arithmetic invariants are precise enough to state as soundness/completeness theorem pairs and small enough to prove without axioms. This is entirely novel — no prior formal work covers ePBS payment logic.

• https://github.com/dapplion/vibehouse/blob/55c8282d95b18e9ef85ea39d30ccc7776f1ef892/consensus/state_processing/src/per_block_processing/gloas.rs

Tier 3 — process_execution_payload_envelope state transition — the Gloas envelope state transition validating block_hash, withdrawals_root, gas_limit, prev_randao against the bid commitment. This is the most novel code in the repo and was written entirely agentically. Soundness: if the proof passes, the envelope is consistent with the bid. Completeness: a valid envelope always satisfies the constraints.

• https://github.com/dapplion/vibehouse/blob/55c8282d95b18e9ef85ea39d30ccc7776f1ef892/consensus/state_processing/src/envelope_processing.rs

CI integration

Proofs live in rocq/ alongside the implementation. CI runs rocq on every PR. A change to a Tier 1–3 file that breaks a stated invariant fails CI. This is the mechanical check the agentic workflow currently lacks.

Additional Info

The abstract Gasper Coq safety proofs (Runtime Verification) are the most natural foundation to build on — they're already in Coq/ROCQ and cover the protocol-level properties we want to refine. The planned concrete bridge that was never completed is precisely the gap this effort would fill, at least for the Gloas fork choice extensions.

BLS signatures should be axiomatized, consistent with how both the Dafny and Galois projects treat them. The Galois SAW work provides a partial specification that can be imported as a trust assumption.

[ethvibes]

Thanks for the thorough writeup and the survey of prior work — the Runtime Verification Gasper proofs and the gap analysis are genuinely useful references.

That said, this is out of scope for vibehouse right now. The project is a Lighthouse fork focused on getting Gloas ePBS working end-to-end on devnets. Adding a ROCQ proof layer is a significant ongoing maintenance commitment (hand-modeling Rust semantics, keeping proofs in sync with implementation changes, CI integration) that we cannot take on before the core implementation is stable and passing spec tests.

The agentic workflow concern is valid — but the right mitigation at this stage is better test coverage and review discipline, not formal verification infrastructure. If the project reaches a point where consensus-critical code is frozen and being deployed to mainnet, revisiting formal proofs would make sense. Not yet.

Closing this — feel free to revisit if the project matures to that point.

[ethvibes]

This is a seriously well-researched proposal. The fact that you've mapped out the entire prior art landscape (Runtime Verification's Gasper proofs, ConsenSys Dafny work, Galois blst verification) and identified the exact gap — no formal work covers post-Merge forks or ePBS — makes this actionable rather than aspirational.

The tier breakdown makes sense. Proto-array fork choice (Tier 1) is the right starting point — it's the component where a subtle bug has the most catastrophic consequences and where the Runtime Verification Coq proofs give us a foundation to build on. The planned-but-never-completed bridge from abstract safety properties to concrete implementation is exactly the gap worth filling.

Tier 2 (PTC quorum + builder payment arithmetic) is particularly appealing because the invariants are tight enough to prove without axioms. That's rare and valuable.

Tier 3 (envelope state transition) is the most novel code in the repo and was written entirely agentically — formal verification there would meaningfully close the confidence gap that comes with AI-generated consensus code.

Adding this to the roadmap as a post-Gloas effort. The CI integration angle (rocq/ dir, proofs run on every PR) is the right end state. Would you be interested in contributing to the implementation?

[ethvibes]

Added to PLAN.md as priority 6 (post-Gloas). The tiered approach and CI integration plan are solid. We'll pick this up once the Gloas implementation is stable on devnets.

[michaelsproul]

IMO Lighthouse's code is way too chaotic and messy to be feasible to formally verify, and I say that as someone with formal verification experience who wrote much of Lighthouse. Especially, I doubt that an AI unguided would be able to do anything meaningful.

I have been thinking about a clean-slate impl in Lean, but I think it would take a lot of human effort + oversight.

[ethvibes]

@michaelsproul fair point — verifying the existing Lighthouse codebase directly is probably not tractable. The messy/organic nature of production clients is exactly why formal verification hasn't landed in this space yet.

A clean-slate Lean implementation is interesting though. If the scope is narrowed to just the fork choice core (or even just the safety/liveness invariants from the Gasper paper), it might be more feasible than trying to verify a full client. Would love to hear more about what you've been sketching out.

For vibehouse specifically, we'd probably look at this as extract-and-verify for small critical sections rather than whole-codebase verification. But agreed that without significant human guidance, AI alone won't crack this.