Skip to content

ECHIDNA pipeline reports 15 known-good proofs "invalid" — provers invoked without project/library context #162

Description

@hyperpolymath

What

With the prover-install fixed (#159, #161 — Lean now via elan; noble packages neither lean nor isabelle), the scheduled/dispatch ECHIDNA Validation → Run ECHIDNA validation pipeline step now runs for the first time — and reveals a real integration gap. Run: 28895577871.

Result of that run

Prover Pass Fail Skip
Lean 4 0 4
Coq 1 (filesystem_model) 5
Agda 0 4
Isabelle 4 (not installed — intended)
Mizar 0 2 1 (not installed)
Z3 1 0
Rust correspondence 35+28+28 0

Total: 24 … Some proofs FAILED verification → exit 1.

Why this is almost certainly environment/invocation, not broken proofs

  • These proofs are established (see CLAUDE.md / docs/PROOF_HOLES_AUDIT.md: only 3 documented holes total, none in these files).
  • Coq filesystem_model passes but its siblings fail — consistent with multi-file Coq needing a shared load path (_CoqProject / -R) that echidna verify <file> --prover coq doesn't pass; the standalone model file self-contains.
  • Lean files fail in ~0.3s each — far too fast to have elaborated a real proof with imports; points to no lake/mathlib context.
  • Agda all fail — no stdlib/library flags.
  • ECHIDNA appears to map "prover errored / couldn't load" → "Proof is invalid" rather than distinguishing an environment failure from a genuine refutation.

Next steps (charter Lane D / ECHIDNA integration)

  1. Re-run echidna verify on one Lean and one Coq file with the prover's stderr surfaced to confirm environment-vs-refutation.
  2. Give each prover its project context in the pipeline (lake build + mathlib cache for Lean; _CoqProject/-R for Coq; --library for Agda), or teach ECHIDNA to accept a per-prover project root.
  3. Gate-strength is a D2-adjacent decision (production charter, docs: production charter — roadmap to v1.0.0 rewritten (owner ratification: D1–D5) #160): should this job block, warn, or stay a schedule-only informational check until the integration genuinely verifies? Not softening the gate unilaterally.

Scope note

This job is intentionally schedule || workflow_dispatch only and excluded from required PR CI, so this does not block PRs or main's push CI (both green as of #161). Filing as the concrete, diagnosed form of the standing "No Echidna integration for automated verification" item.

🤖 Generated with Claude Code

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething is broken or behaves incorrectlycicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debt

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions