roadmap: Multi-prover consensus voting (v1.0.0 long-term)

[hyperpolymath]

Origin

ROADMAP.adoc §"Long-Term Goals (v1.0.0 -- Q3-Q4 2026)", "Multi-Prover Consensus" (lines 149-153):

=== Multi-Prover Consensus

• Configure N provers to verify each proof
• Consensus voting (majority must agree)
• Disagreement reporting

Scope

Three bullets, one tracker:

1. Configurable N-prover dispatch: per-PR / per-repo config selects N provers (e.g. Coq + Lean + Isabelle for a .v-flavoured theorem)
2. Majority voting: N/2+1 must agree on Verified / Failed before the result is reported back to the PR
3. Disagreement reporting: when the vote splits, surface a structured disagreement report (which prover said what, with timing/axiom data) so the human reviewer can adjudicate

This is the trust-redundancy track. Today's echidnabot picks a single prover per theorem; consensus mode is the platform feature that makes "we are sure" defensible. PR count not estimated in roadmap; rough order: ~5-8 PRs.

Dependencies

• Builds on top of echidna's existing portfolio solving (src/rust/verification/portfolio.rs) — that primitive answers "first to succeed wins"; consensus is the inverse "all must agree" semantic
• Cross-prover proof exchange (echidna Stage 6a OpenTheory / 6b Dedukti) helps make disagreement explanations machine-readable but is not strictly required
• No upstream blocker

Why filed

To make the v1.0 "Multi-Prover Consensus" commitment trackable. Today the three bullets live only as a checklist in ROADMAP.adoc with no issue. This is the differentiating feature for echidnabot vs single-prover competitors and deserves a visible tracker.