Phase 3 nudge — KeYmaera X et al still outstanding

[hyperpolymath]

Status check — 2026-04-30

Phase 3 was reserved on 2026-04-27 for an interactive Opus session. This is the scheduled nudge.

Backend file check

Backend	File	Status
KeYmaera X	src/rust/provers/keymaera_x.rs	✗ missing
QEPCAD-B	src/rust/provers/qepcad.rs	✗ missing
Redlog	src/rust/provers/redlog.rs	✗ missing
MleanCoP	src/rust/provers/mleancop.rs	✗ missing
ileanCoP	src/rust/provers/ileancop.rs	✗ missing
nanoCoP	src/rust/provers/nanocop.rs	✗ missing
MetTeL2	src/rust/provers/mettel2.rs	✗ missing

STATE.a2ml has no phase-3 block — phase not recorded as started or complete.

Why this needs an interactive Opus session

Do not farm these out to a bulk or mechanical agent. Two of the seven require real architectural reasoning:

• KeYmaera X — differential-dynamic-logic semantics; the backend needs to understand dL proof obligations, Pegasus arithmetic sub-calls, and the Mathematica/Z3 oracle tier. Getting the trust-tier classification (Tier 4, small-kernel via Pegasus + Mathematica/Z3) right requires genuine understanding of what dL certificates look like.
• Redlog — runs inside the Reduce CAS, not as a standalone binary; requires a subprocess shim that speaks the Reduce REPL protocol. The integration pattern is unlike any of the existing 105 backends.

The other five (MleanCoP, ileanCoP, nanoCoP, MetTeL2, QEPCAD-B) are more mechanical but should be done in the same session for coherence.

Reference material

• Roadmap: .machine_readable/6a2/STATE.a2ml → [expansion-roadmap] block
• Backend templates: src/rust/provers/dafny.rs and src/rust/provers/gnatprove.rs
• Trust tier guide: src/rust/verification/ (confidence scoring, 5-level hierarchy)

Expected trust-tier classifications (for the Opus session to verify)

• KeYmaera X = Tier 4 (small-kernel via Pegasus + Mathematica/Z3)
• QEPCAD-B = Tier 1 (external-subprocess CAS, Saclib build)
• Redlog = Tier 1 (subprocess via Reduce CAS)
• MleanCoP / ileanCoP / nanoCoP = Tier 2 (Prolog-based connection-method)
• MetTeL2 = Tier 2 (JVM, tableau generator)

Next step

Pick a 2–3 hour Opus session this week to do the 7 Phase 3 backends. When complete, update .machine_readable/6a2/STATE.a2ml with a [[expansion-roadmap.phase]] block for id = "phase-3", set status = "complete", and add a landed date.

---

Auto-generated by scheduled Phase 3 status-check agent — 2026-04-30