roadmap: Distributed proof verification on K8s (v1.0.0 long-term)

[hyperpolymath]

Origin

ROADMAP.adoc §"Long-Term Goals (v1.0.0 -- Q3-Q4 2026)", "Distributed Proof Verification" (lines 155-159):

=== Distributed Proof Verification

• Kubernetes-native horizontal scaling
• Proof job distribution across workers
• Worker health monitoring

Scope

Three bullets, one tracker:

1. K8s-native horizontal scaling: a Deployment + HorizontalPodAutoscaler that scales worker pods on queue depth
2. Proof job distribution: a queue (NATS/Redis Streams) with worker-side pull semantics; per-job affinity (pin Coq jobs to Coq-warm workers when image weight matters)
3. Worker health: liveness/readiness probes that distinguish "prover binary healthy" from "container alive"; per-prover health bit so a sick Lean worker doesn't poison the rotation

This is the horizontal-scale track. Single-instance echidnabot caps at the box's CPU; distributed mode is the path to "we verify the entire estate's PRs in one place". PR count not estimated in roadmap; rough order: ~8-12 PRs (queue layer + worker pool + K8s manifests + health checks + tests).

Dependencies

• Echidnabot v0.2.0 Deployment (Medium Priority) work must land first — the Docker Compose / Podman / Helm tracks (ROADMAP.adoc:131-135) are prerequisites for any K8s story
• Pre-built Podman images for all 12 provers (ROADMAP.adoc:132) — workers need to start fast, image pulls dominate cold-start latency without prebuilt images
• No upstream blocker beyond the prerequisite Deployment work

Why filed

To make the v1.0 "Distributed Proof Verification" commitment trackable. Today the three bullets live only as a checklist in ROADMAP.adoc with no issue. The K8s scaling story is the platform feature that turns echidnabot from a per-repo bot into estate infrastructure.