Roadmap

Roadmap

Short summary; the authoritative version is ROADMAP.adoc at the root.

Now (post v1.0.0-alpha)

• ✅ Both pillars machine-checked across six provers + Idris (PR #100) — proofs/verify-all-provers.sh
• ✅ OND pillar authored (OND-1..5 proved, zero axioms); ✅ Idris ABI builds; ✅ Isabelle + Mizar verify
• Wire proof verification into CI (.github/workflows/proofs.yml runs Coq + Z3; extend to more provers)
• Discharge the class-A remainder (needs finite-dim/tensor QM + coinductive-β machinery) — optional
• Prove OND-6 (conditional composition) — the research capstone

Next (v0.9 → v1.0 milestones)

• v0.9.0 — Container / CI proof verification: Containerfile with all six provers, cross-arch CI
• v1.0.0 — Publication: paper (both pillars, six-prover story), industrial CNO/OND examples

Long horizon (v2 → v12)

7-year vision: language expansion, AI-assisted proving, quantum verification, standardisation. Detailed phase decomposition in ROADMAP.adoc.

How decisions are recorded

• Forward-looking architectural choices → ADRs in .machine_readable/descriptiles/META.a2ml architecture-decisions section
• Backward-looking audit events → AUDIT.adoc
• Live phase / progress → .machine_readable/descriptiles/STATE.a2ml