Add MVP 1.0 checklist and smoke checks

Author: Jonathan D.A. Jewell

CHANGELOG.adoc

@@ -115,11 +115,11 @@ ECHIDNA follows Semantic Versioning (SemVer):
 - DeepProbLog integration
 - Performance optimizations
 
-=== [1.0.0] - Target: 2026-11-22
-- Tier 4 prover implementation (HOL4)
-- Complete 12-prover support
-- Production-ready release
-- Comprehensive documentation
+=== [1.0.0] - Target: ASAP
+- Complete 12-prover support (core 12)
+- CLI + HTTP API MVP
+- MVP smoke checks
+- Documentation updated for 1.0
 
 == Migration Notes
 

Justfile

@@ -75,3 +75,7 @@ audit:
 # All checks before commit
 pre-commit: fmt-check lint test
     @echo "All checks passed!"
+
+# MVP 1.0 smoke checks
+mvp:
+    ./scripts/mvp-smoke.sh

README.adoc

@@ -257,6 +257,6 @@ If you use ECHIDNA in your research, please cite:
 
 ---
 
-*Version*: 0.1.0
-*Status*: Active Development
-*Last Updated*: 2026-01-10
+*Version*: 1.0.0 (MVP target)
+*Status*: MVP Drive (All Provers + CLI/API)
+*Last Updated*: 2026-01-18

docs/MVP-1.0.adoc

@@ -0,0 +1,61 @@
+= ECHIDNA MVP 1.0 Checklist
+:toc: macro
+:toclevels: 2
+
+This checklist defines the minimum shippable scope for ECHIDNA 1.0.
+
+TOC::[]
+
+== Scope
+
+* All 12 core provers are wired and available via CLI + HTTP API.
+* CLI supports prove/verify/search/interactive/server.
+* HTTP API exposes health, provers, prove/verify/suggest/search, sessions.
+* Basic smoke checks exist for prover executables and pipeline paths.
+* Release documentation is updated and consistent.
+
+== Prover Coverage (Core 12)
+
+* Agda
+* Coq
+* Lean
+* Isabelle
+* Z3
+* CVC5
+* Metamath
+* HOL Light
+* Mizar
+* PVS
+* ACL2
+* HOL4
+
+== CLI
+
+* `echidna prove` works for each prover (file-based proof).
+* `echidna verify` works for each prover.
+* `echidna search` works (at least for provers with theorem DBs).
+* `echidna interactive` starts for each prover.
+* `echidna server` starts API server and serves endpoints.
+
+== HTTP API
+
+* `GET /api/health` returns OK + version.
+* `GET /api/provers` lists all 12 core provers.
+* `POST /api/prove` accepts payload + returns success.
+* `POST /api/verify` accepts payload + returns success.
+* `POST /api/suggest` returns tactics (or explicit “not available”).
+* `GET /api/search` returns matches (or explicit “not available”).
+* `POST /api/session/create` creates a session.
+* `GET /api/session/:id/state` returns state.
+* `POST /api/session/:id/apply` applies tactic.
+
+== Smoke Tests
+
+* Script exists to check prover executables are available (or clearly report missing).
+* Script runs minimal prove/verify for each prover when available.
+
+== Release Prep
+
+* `README.adoc` updated for 1.0 MVP.
+* `CHANGELOG.adoc` updated for 1.0 MVP.
+* Tagging plan for `v1.0.0`.

scripts/mvp-smoke.sh

@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+BIN="${ROOT_DIR}/target/release/echidna"
+
+if [[ ! -x "$BIN" ]]; then
+  echo "[MVP] echidna binary not found: $BIN"
+  echo "[MVP] Build with: cargo build --release"
+  exit 1
+fi
+
+PROVERS=(
+  agda coq lean isabelle z3 cvc5 metamath hollight mizar pvs acl2 hol4
+)
+
+missing=()
+
+check_cmd() {
+  local cmd="$1"
+  if ! command -v "$cmd" >/dev/null 2>&1; then
+    missing+=("$cmd")
+  fi
+}
+
+# Basic executable checks (best-effort: many provers are optional installs)
+check_cmd agda
+check_cmd coqtop
+check_cmd lean
+check_cmd isabelle
+check_cmd z3
+check_cmd cvc5
+check_cmd metamath
+check_cmd hol-light
+check_cmd mizar
+check_cmd pvs
+check_cmd acl2
+check_cmd hol4
+
+if [[ ${#missing[@]} -gt 0 ]]; then
+  echo "[MVP] Missing executables: ${missing[*]}"
+fi
+
+# Minimal list-provers check
+"$BIN" list-provers >/dev/null
+
+# Minimal health for server startup is manual; keep smoke lightweight
+
+echo "[MVP] Smoke checks completed (missing executables are expected on dev machines)."