Roadmap
Edit on GitHubProject-level phase ledger, the per-program milestone history (Cats Effect 3 migration, translator soundness, test generation, synthesis), the per-pipeline capability inventory, the live follow-up backlog, and the wontfix decisions of record.
Last updated:
This page is the single source of truth for project status. Every other page in this site focuses on how a pipeline works; this page answers what's done, what's planned, and what's intentionally not coming. It is regenerated from the per-page status content that used to live in Architecture, Verification Engine, Test Generation, and Synthesis Pipeline; those pages now link here for status questions.
Project phases
phase-N issue labels gate each entry. "Shipped" means merged on main and continuously
hardened by the workflows under .github/workflows/. "Not started" means an issue thread
exists but no code has merged.
| Phase | Theme | Status |
|---|---|---|
| 1 | Core parser / IR build | Shipped. ANTLR4 grammar at modules/parser/src/main/antlr4/Spec.g4; Parse.parseSpec -> Builder.buildIR returns IO[Either[VerifyError, ServiceIR]]. |
| 2 | Convention engine (M1-M10) | Shipped. Operation classification + naming/path/schema/validate at modules/convention/; see Convention Engine. |
| 3 | python-fastapi-postgres codegen + Alembic + OpenAPI | Shipped. See python-fastapi-postgres for the deployment-target spec. |
| 4 | Verification (Z3 + Alloy + Isabelle/HOL universal soundness) | Shipped. Pivoted from Lean 4 to Isabelle/HOL via #193; IR canonicalized in #202; production verify routes in-subset checks through the Isabelle-extracted translator (#192). See Verification capabilities below. |
| 5 | Test generation (native, per-target) | Largely shipped. M5.2 stateful, M5.3 structural, M5.4 conformance runner, M5.6 custom strategies, M5.8 sensitive fields, M5.9 transitions, M5.10 built-in predicates all on main. M5.11 multi-target native conformance shipped: the Backend.scala seam emits the suite in each target's own language (pytest+Hypothesis+Schemathesis / Vitest+fast-check / go test+rapid) with Python as the byte-identical differential oracle (#278, #279, #280; closes #265). See Test generation follow-ups. |
| 6 | LLM / Dafny synthesis (CEGIS) | Shipped through M6.7. Operation classification (#31), Dafny signature generation (#32), LLM integration (#28), CEGIS loop (#29), compile --with-synthesis (#27), graduated fallback (#30), DafnyPro-style hint augmentation (#229). See Synthesis follow-ups. |
| 7 | Multi-target codegen, Go/chi, TS/Express | Shipped. Go/chi target shipped in #33; see go-chi-postgres. TS/Express target shipped in #35; see ts-express-postgres. CLI polish shipped in #36: compile --dry-run, diff, test, --color/--no-color, exit-code reference; see CLI Reference. Distribution shipped in #34: 4-platform release binaries (linux-amd64, macos-arm64, macos-amd64, windows-amd64), GHCR Docker image (ghcr.io/hardmax71/spec-to-rest), and a composite GitHub Action; see Install. Diff migrations across all three targets shipped in #56: snapshot-driven Alembic / golang-migrate / Prisma deltas with reversible up/down; see Migrations. Alternative database dialects shipped in #58: python-fastapi-sqlite and python-fastapi-mysql profiles via a pluggable Dialect strategy (per-dialect SQLAlchemy types, triggers, partial-index handling, connection/compose wiring). Schema-derivation polish shipped in #57: derived and recalculated fields emit SQL CREATE TRIGGER statements, and where-qualified indexes emit as partial indexes, handled per-dialect by the Dialect strategy. Protected regions and extension files for safe regeneration shipped in #62. Multi-environment Compose overrides (staging/prod) shipped in #63. Readiness and metrics routes shipped in #500: every generated service exposes GET /ready (database-probe readiness, 200/503) and a Prometheus GET /metrics endpoint alongside /health, instrumented per target with the standard client library. The generated-vs-hand-written benchmark CI job (#64) was closed not-planned (maintenance-sync burden; see the Closed not-planned section below). |
| 8 | Authentication DSL | Shipped. Service-wide security { ... } blocks and per-operation requires_auth: clauses parse into the IR (M8.1 (#53)); see Spec Language, Security schemes. Declared schemes emit into OpenAPI securitySchemes (M8.2 (#54)). Per-scheme runtime guards (Bearer / ApiKey / Basic) are wired across all three targets, FastAPI, Go/chi, and TS/Express (M8.3 (#55)). |
Recent milestones
History of internal milestone identifiers and the issue/PR they shipped through. Use this
to map a section title like ## Hint-Augmentation (M6.7) back to the activation issue and
closure date. Older completed milestones are summarised; newer ones get a one-line
context.
M_CE.*, Cats Effect 3 migration
Umbrella: #95
| Milestone | Theme | Closed |
|---|---|---|
| M_CE.1 (#96) | Cats Effect 3 build dep + munit-cats-effect test harness | shipped |
| M_CE.2 (#97) | Typed VerifyError ADT across parse/build/translate/backend | shipped |
| M_CE.3 (#98) | Resource[IO, _]-managed Z3 / Alloy / dump-sink backends | shipped |
| M_CE.4 (#99) | Pipeline entries return IO[Either[VerifyError, _]]; Consistency.runConsistencyChecks returns IO[ConsistencyReport] | shipped |
| M_CE.5 (#100) | Parallel check dispatch (parTraverseN, --parallel <n>) | shipped |
| M_CE.6 (#101) | Cancel-aware Resource lifecycle for Z3 and Alloy backends | shipped |
| M_CE.7 (#102) | spec-to-rest as CommandIOApp, structured IO[ExitCode], SIGINT wired to fiber cancellation | shipped |
| M_CE.8 (#103) | Single-API pipeline, synchronous wrappers removed, tests on CatsEffectSuite | shipped |
| M_CE.9 (#104) | Concurrency docs + JMH ParallelVerifyBench with fixtures/golden/bench/parallel_verify.csv | shipped |
M_L.*, Translator soundness
Issue #88 closed 2026-04-26 after decomposition into M_L.0-M_L.4 + the global-proof umbrella #170. The Isabelle/HOL pivot #193 sealed the production cutover. See the translator soundness writeup for the trust-chain framing.
| Milestone | Theme | Closed |
|---|---|---|
| M_L.0 (#126) | Scope, scaffolding, contributor handoff | shipped |
| M_L.1 (#127) | IR denotational semantics for verified subset (Semantics.thy) | shipped |
| M_L.2 (#128) | Translator soundness theorem for verified subset | shipped |
| M_L.3 (#129) | Per-run certificate emission | shipped, then deleted post-pivot because universal soundness made it vestigial |
| M_L.4 (#130) | Subset expansion (a-l, including M_L.4.l IndexRel widen #210) | shipped |
| Isabelle pivot (#193) | Lean -> Isabelle/HOL + Code_Target_Scala; universal soundness theorem closes with zero sorry | shipped |
| IR canonicalization (#202) | Full input-language IR in Isabelle; lower :: expr_full => expr option projection; flat case-class extraction | shipped |
| Trust dimension (#205) | Per-check trust: "sound" | "best-effort"; new exit code 4 (ExitStatus.Trust); JSON schemaVersion 1->2 | shipped |
| Production routing (#192) | ExpressionEncoder.translateCheckedExpr routes in-subset check bodies through SpecRestGenerated.translate and SmtTermBridge; the Scala fallback is isolated to declaration-level expressions | shipped |
| Codegen drift gate (#231) | isabelle-build.yml regenerates SpecRestGenerated.scala and diffs against the committed copy on every PR | shipped |
| One-IR collapse (#391) | The expr_full/expr twin pipeline and the lower projection collapsed into a single verified expr (27 constructors); direct soundness (translate_soundness_standalone in soundness/DirectSound.thy) replaces the lower-then-translate chain | shipped |
M5.*, Test generation
| Milestone | Theme | Closed |
|---|---|---|
| M5.2 | Stateful tests (Hypothesis state machine) | shipped |
| M5.3 | Structural tests (Schemathesis) | shipped |
| M5.4 | Conformance runner (tests/run_conformance.py) | shipped |
| M5.6 | Custom strategies (per-field @strategy) | shipped |
| M5.8 | Sensitive fields (PII redaction in test logs) | shipped |
| M5.9 | Transition tests (from/to/when transition rules) | shipped |
| M5.10 | Built-in predicates (isValidURI, regex matches, len()) | shipped |
| M5.11 (#278 / #279 / #280) | Native multi-target conformance: Backend.scala seam (ExprBackend/StrategyBackend/HarnessTemplates); ts-express Vitest+fast-check, go-chi go test+rapid, structural-lite for both; Python byte-identical oracle (closes #265) | shipped |
| M5.12 (#140) | Test emission on by default for every supported target; the --with-tests flag dropped, --no-tests is the opt-out | shipped |
| Temporal predicates (#86) | Runtime artifacts for always(P) / eventually(P) | shipped |
| Guarded positive transitions (#152) | GuardSatisfier for predicate-conditional transitions | shipped |
| Per-status bundles for transition-driven entities (#153) | Schemathesis bundle routing by status | shipped |
Body and query inputs on via operations (#155) | Operation-input plumbing for transition tests | shipped |
M6.*, LLM synthesis
| Milestone | Theme | Closed |
|---|---|---|
| M6.1 (#31) | Operation classification, DIRECT_EMIT vs LLM_SYNTHESIS | shipped |
| M6.2 (#32) | Dafny signature generation; inspect --format dafny[-prompt] | shipped |
| M6.3 (#28) | LLM integration + prompt engineering; synth try | shipped |
| M6.4 (#29) | CEGIS feedback loop wired to dafny verify --log-format json; synth verify | shipped |
| M6.5 (#27) | compile --with-synthesis, Dafny -> target translation, splice into Python project | shipped |
| M6.6 (#30) | Graduated fallback, L1 prompt ladder + L3 model escalation + L4 skeleton + L5 report; L2 deferred | shipped |
| M6.7 (#229) | DafnyPro-style hint augmentation in repair prompts; replaces the originally planned #227 L2 path (closed wontfix-with-pivot, see the compositional synthesis findings) | shipped |
Other shipped infrastructure
- Cross-solver verdict agreement (#131), native cvc5 cross-check job in CI replays each per-check
.smt2and asserts agreement with the recordedrawStatus. - Property-based translator tests (#162),
TranslatorPropTest.scalaruns 50 random IRs/property over the verified subset. - Typed
__init__(body)on ORM,SecretStrat the schema boundary (#212), Python codegen ergonomics. - Isabelle codegen drift gate (#231),
isabelle-build.ymlre-extracts anddiffs against the committedSpecRestGenerated.scalaon every PR.
Verification capabilities
Per-feature ledger for the verifier. For the prose explanation of each entry, see Verification Engine.
Capability ledger
| Capability | Status |
|---|---|
| IR-to-SMT translator (entities, enums, state relations, invariants) | shipped |
Synchronous Java Z3 backend + spec-to-rest verify CLI | shipped |
| Invariant-satisfiability smoke check | shipped |
SMT-LIB artifact export (--dump-smt) | shipped |
Invariant consistency checking (per-op requires, dead ops) | shipped |
Primitive-type alias refinement (type Positive = Int where ...) | shipped |
Scalar type sorts (Int/Bool; temporal DateTime/Date as epoch Int; fractional Float/Decimal/Money as Real) | shipped (Z3; ordering and arithmetic over these verify, with Int/Real coercion; non-numeric primitives stay uninterpreted, so ordering/arithmetic on them is skipped as outside the encodable subset, not crashed) |
Cardinality on state relations (#store, uninterpreted >= 0) | shipped |
| Invariant preservation checking (operation pre/post => invariant) | shipped |
Prime (X'), Pre(X), With record update, inline y in {...} | shipped |
| Two-world state encoding + smart frame synthesis | shipped |
| Cardinality pre/post delta axioms (insert / delete / identity) | shipped |
| Counterexample-driven diagnostics (spans, entity/state decoding) | shipped |
| Category-based error reporting + per-category suggestion hints | shipped |
| Verify-as-gate (refuse codegen on failed verification) | shipped (#78), compile runs verify by default; --ignore-verify opts out |
Machine-readable (--json / --json-out) diagnostics output | shipped |
Richer suggested-fix templates (op/invariant/field-aware; opt-out via --no-suggestions) | shipped |
Human-readable "why this fails" narration (opt-out via --no-narration) | shipped (#89), covers invariant_violation_by_operation, contradictory_invariants, unreachable_operation |
| Structural spec lints (type mismatch, unused entity, ...) | shipped, check runs L01-L06 (#81); L04 ships a syntactic over-approximation, SAT-based overlap is candidate verify-side work |
Per-check VC dump (--dump-vc <dir>), Z3 SMT-LIB and Alloy .als artifacts | shipped |
Unsat-core extraction (--explain), surface contributing spec spans on unsat diagnostics | shipped (Z3 always; Alloy when minisat.prover is bundled) |
| Native Alloy CLI cross-check job in CI | shipped |
| Native cvc5 cross-check job in CI (cross-solver verdict agreement) | shipped (#131), replays each per-check .smt2 through native cvc5 and asserts agreement with the recorded rawStatus |
Set-literal membership (x in {A, B, C}), set algebra (union, intersect, minus, subset), non-state set membership via (select ...) | shipped (Z3) |
Standalone set comprehension as equality RHS (s = {x in D | P}) | shipped (Z3, via extensional sort-coerced quantifier axiom; requires binder element sort to match receiver element sort) |
Powerset (^s), existential binder (some t in ^s | P(t)) | shipped (Alloy, bounded scope; default 5) |
Powerset (^s), universal binder (all t in ^s | P(t), no t in ^s | ...) | sharp error, Alloy rejects as higher-order-non-skolemizable regardless of body; rewrite as existential or as a first-order statement about s |
Alloy-routed requires / enabled / preservation (invariants or ensures using ^) | shipped, two-world preservation encoding (State + StatePost sigs, frame synthesis, negated post-invariant). Note: Alloy cannot discharge preservation when the invariant's negation is itself a universal over a powerset |
Alloy source export (--dump-alloy, --dump-alloy-out) | shipped |
Temporal always(P), P holds in every state satisfying the invariants | shipped (Alloy, bounded scope; implemented as I and not P unsat-check). Runtime artifacts: temporal_always_<name> per-op behavioral test + @invariant() block in stateful test + x-temporal OpenAPI extension (see Test Generation section 4) |
Temporal eventually(P), some state satisfies P and the invariants | shipped (Alloy, bounded scope; implemented as I and P sat-check). Runtime artifacts: stateful state machine emits a _eventually_seen_<name> flag in _reset, an @invariant() observer that flips it when P holds, and a teardown(self) method that asserts the flag (see Test Generation section 4). Strictly weaker than the Alloy proof, bounded by per-case trace length |
Temporal fairness(op) | not supported in v1, sharp error; requires trace-based verification via Alloy's var-sig mode (future work). No runtime artifacts emitted; testgen records a _testgen_skips.json entry instead |
Cats Effect 3 build dependency + munit-cats-effect test harness | shipped in M_CE.1 (#96) |
Typed VerifyError ADT across parse/build/translate/backend | shipped in M_CE.2 (#97) |
Resource[IO, _]-managed Z3 / Alloy / dump-sink backends | shipped in M_CE.3 (#98) |
Pipeline entries (Parse.parseSpec, Builder.buildIR, Z3/Alloy Translator.*, WasmBackend.check, AlloyBackend.check) return IO[Either[VerifyError, _]] | shipped in M_CE.4 (#99) |
Consistency.runConsistencyChecks returns IO[ConsistencyReport] (per-check failures remain data inside the report, not in the Either channel) | shipped in M_CE.4 (#99) |
Parallel check dispatch (parTraverseN, --parallel <n>) | shipped in M_CE.5 (#100) |
Cancel-aware Resource lifecycle for Z3 and Alloy backends (per-check timeouts enforced inside the solvers) | shipped in M_CE.6 (#101) |
spec-to-rest as CommandIOApp, structured IO[ExitCode] subcommands, SIGINT wired to fiber cancellation | shipped in M_CE.7 (#102) |
Single-API pipeline, every Parse, Builder, Translator, WasmBackend, AlloyBackend, and Consistency entry point returns IO; synchronous wrappers removed; test suites migrated to CatsEffectSuite with per-module SpecFixtures.loadIR helpers | shipped in M_CE.8 (#103) |
Concurrency docs (docs/content/docs/pipelines/concurrency.mdx) + JMH ParallelVerifyBench with checked-in CSV at fixtures/golden/bench/parallel_verify.csv | shipped in M_CE.9 (#104) |
Property-based tests for the Z3/Alloy translators (translation determinism on identical IRs, free-identifier resolution against TranslatorArtifact, structural invariant preservation between Z3 and Alloy) via scalacheck-effect-munit | shipped (#162), modules/verify/src/test/scala/specrest/verify/TranslatorPropTest.scala runs 50 random IRs/property over the verified subset from the translator soundness writeup |
Mechanically verified translator soundness in Isabelle/HOL: universal translate_soundness_standalone theorem in proofs/isabelle/SpecRest/soundness/DirectSound.thy closes with zero sorry over the verified subset; Code_Target_Scala extracts translate and the canonical IR ADT to modules/ir/src/main/scala/specrest/ir/generated/SpecRestGenerated.scala | shipped via the Isabelle pivot (#193); IR canonicalized in #202; two-level IR collapsed into one verified expr in #391; CI runs isabelle build SpecRest per PR via .github/workflows/isabelle-build.yml. Per-run cert emission deleted post-pivot, universal soundness made it vestigial. |
Per-check Trust dimension, each CheckResult carries trust: "sound" | "best-effort" driven by the extracted Isabelle trustGlobal/trustRequires/trustEnabled/trustPreservation classifiers (membership in the translate domain); best-effort checks short-circuit to Skipped (category=soundness_limitation) before backend dispatch; new exit code 4 (ExitStatus.Trust, unified from the former ExitCodes facade by #421) | shipped (#205), JSON schemaVersion 1->2 |
Production verify path routes in-subset checks via the extracted (Isabelle-verified) translator: translateCheckedExpr uses SpecRestGenerated.translate >>> SmtTermBridge and fails instead of falling back on None; translateDeclarationExpr is the separate fallback path for declaration-level refinements. Best-effort checks at the verify level always skip with soundness_limitation (no flag) | shipped (#192) |
Synthesis follow-ups
Open follow-ups for the M6 synthesis pipeline. For the prose context, see Synthesis Pipeline.
| Concern | Tracked in |
|---|---|
Dafny ServiceState reconciliation (the kernel used to run on fresh per-request state) | shipped for all three targets in #511, #512, #513; CI runs the synthesized url_shortener conformance suites since #514. Kernel handlers hydrate state from the database, check the compiled Requires twins, and persist mutations in one transaction. Nullable and seq state crossed the go/ts bridges in #518; enum fields, scalar collections, query-param kernel ops, and entity/list output shapes followed on all three targets, so todo_list runs every operation on verified kernels fleet-wide. Nested entity collections landed next: ecommerce's items: Set[LineItem] hydrates by joining the element rows against the id-list column, optional int query params cross the boundary, and ecommerce runs ten of its eleven operations on verified kernels (RemoveLineItem's definite description over an order's item set stays on the fail-loud stub until TheBy learns set domains). The kernel bodies are Dafny-verified through synth accept, with provenance recorded per cache entry. Keyed hydration followed in #522: a static contract analysis (HydrationScope) scopes each request to the rows its requires and ensures actually touch, so an UpdateTodo loads one row instead of the table, inserts hydrate nothing, and the persist delete scan is confined to hydrated rows. The scope is then closed under the service invariants, since the runtime guard and the kernel's precondition evaluate ServiceStateInv on the hydrated state: relations an invariant reads outside its own rows load whole, which keeps per-row specs (todo_list, url_shortener) fully keyed while densely cross-referenced ones (ecommerce's orders/payments cycle) fall back toward full loads until reverse-reference keyed loads land. Content searches, freshness checks, quantifier scans, and anything the analyzer does not recognize fail open to full hydration. |
Automatic hint discovery, mining proof patterns from verified CEGIS runs instead of hand-curating HintLibrary | follow-up, deferred in the compositional synthesis findings |
Pass@128-scale sampling, raising CegisBudget.maxIterations by an order of magnitude for Re:Form-style gains | follow-up, deferred in the compositional synthesis findings |
Laurel-style assertion localization, inserting assert placeholders at the failing line for the model to fill | follow-up |
Test generation follow-ups
For the prose context, see Test Generation.
| Limit | Tracked under |
|---|---|
| State-dependent preconditions on non-transition ops still skip ensures tests | residual tail of M5.9; not currently scoped |
Guards outside > / >= / < / <= / = literal / != none / their conjunctions | extend GuardSatisfier in Behavioral.scala to cover further patterns case-by-case |
Convention engine follow-ups
Operation shapes the convention engine does not generate yet. Each needs a new convention property plus the codegen behind it; see Convention engine edge cases.
| Shape | Status |
|---|---|
Nested resource creation, auto-detected POST /{parent}/{id}/{child} (M6 / CreateChild) | reserved in the classifier, not emitted; reachable today only via an http_path override |
Idempotency-key handling (Idempotency-Key header plus a dedup store) | not handled |
Multipart and file-upload endpoints for Bytes fields | not handled; the column is generated, the upload route is not |
Asynchronous operations (202 Accepted plus a polling endpoint) | not handled |
| Webhook registration and delivery | not handled |
Tooling follow-ups
| Concern | Status |
|---|---|
| Language server and editor integration (inline diagnostics, completion, go-to-definition) | not built; the only spec-aware tooling today is this site's Shiki highlighter, see errors and developer experience |
Code generation follow-ups
The observability backlog is closed. /health, /ready, and /metrics ship by default since
#500, and every generated service exports
OpenTelemetry spans since #508: set
OTEL_EXPORTER_OTLP_ENDPOINT and each request produces a server span named by its route
template; leave it unset and tracing stays off with nothing wired. See
generated project.
Closed not-planned (decisions of record)
These items have closed issues with explicit rationale; they're not on the roadmap and will not be picked up unless the underlying constraint changes.
- Full Z3 proof-term export (Alethe / Z3-native), #90, closed 2026 not-planned. Z3 has no Alethe export and its native proof format buries quantifier instantiation in opaque steps; superseded by cross-solver agreement (#131) for solver-side defense in depth and by translator-soundness work (#88) for translator-side trust. A 2026-06 re-test put numbers behind the decision. cvc5, the Alethe producer one would reach for since Z3 emits no proofs, was run over the dumped verification conditions of the four hardest specs, 308 checks in all. Even the current build (1.3.4, May 2026) renders a checkable Alethe certificate for only 9 of the 242 properties z3 proves, under 4%. Of the 125 checks cvc5 reproves, 116 fail Alethe export because their proofs reason in the sequence and set theories that the relation and collection encoding compiles to, which the format has no syntax for (
unsupported by Alethe: contains Seq/Set), alongside a skolemization-residue operator with no Alethe form. cvc5 1.1.2 crashed outright on these; 1.3.4 reports them cleanly but still cannot emit them. The reopen trigger is the Alethe specification gaining sequence and set theories, not a newer solver. - L2 operation decomposition for graduated fallback, #227, closed 2026-05-10 wontfix-with-pivot. Replaced by M6.7 hint-augmentation per the literature analysis in the compositional synthesis findings (DafnyComp 7% ceiling, Pass@4 plateau, and about +10pp from hint-augmentation, the component-isolated slice of DafnyPro's +16pp at POPL 2026).
- Benchmark CI job (generated vs hand-written), #64, closed 2026-05-31 not-planned. A latency/LoC comparison needs a hand-written reference service per fixture (and per target) kept in lockstep with an evolving spec language, convention set, and target matrix; that maintenance-sync burden outweighs an explicitly optional quality signal. Correctness is already covered self-maintaining by the default-on conformance suite, the
SkipRateProbeTestskip-rate locks, and themutation-testing.ymlkill-rate gate; GitHub-hosted runners are too noisy for a latency regression gate. A one-off documented measurement, not a maintained CI job, is the better-amortized form if ever wanted.