Architecture

Technology stack

The compiler runs on Scala 3.6.3. ANTLR4 (Java runtime) parses the input via sbt-antlr4. The effect runtime is Cats Effect 3.7; every pipeline stage returns IO and the CLI runs as a decline-effect CommandIOApp (see Concurrency and Cancellation).

Constraint solving uses Z3 Java bindings via tools.aqua:z3-turnkey 4.13, which bundles libz3 natively so no system install is required. A second Z3-vs-cvc5 cross-check job runs in CI (#131). Bounded model checking uses Alloy 6.2 (powerset + temporal always/eventually).

Translator soundness is mechanically verified in an Isabelle/HOL session under proofs/isabelle/SpecRest/. The universal translate_soundness_standalone theorem closes with zero sorry; Code_Target_Scala extracts the verified translator and the canonical IR ADT to modules/ir/src/main/scala/specrest/ir/generated/SpecRestGenerated.scala. The track pivoted from Lean 4 in #193; IR canonicalized in #202; the two-level IR collapsed into one verified expr in #391.

Code generation uses Handlebars templates (handlebars.java) for the python-fastapi-postgres, go-chi-postgres (#33), and ts-express-postgres (#35) targets. Test generation emits a native behavioral/stateful/structural conformance suite under tests/ by default (opt out with compile --no-tests), in the target's own language (pytest+Hypothesis+Schemathesis / Vitest+fast-check / go test+rapid) via the Backend.scala seam, with the Python path held byte-identical as the differential oracle.

Distribution is via GraalVM native-image (sbt-native-image), built by the native.yml workflow. The day-to-day entry point is sbt cli/run ....

Compiler pipeline

The compile pipeline is parse -> IR build -> verify -> convention map -> emit. Property-test generation runs as a sixth stage by default (opt out via --no-tests). The --with-synthesis flag invokes the M6 LLM-synthesis loop: dafny verify-driven CEGIS over LLM-generated bodies (#28, #29) substitutes the verified Dafny output for the raise NotImplementedError stubs in the emitted project (#27). Graduated fallback (#30) and DafnyPro-style hint augmentation (#229) cover the cases where verification needs help. The standalone synth verify subcommand runs the same loop without committing changes back to a project tree.

1. Parse. ANTLR4 grammar (Spec.g4) produces a CST that the builder lowers to a typed IR. The parser auto-injects a short preamble (isValidURI, isValidEmail). See Parser Implementation Notes.
2. IR build. CST becomes ServiceIR, a Scala 3 enum/case-class ADT, with span tracking.
3. Verify. verify runs structural lints (L01-L06; see structural lints) and then translates each obligation to either Z3 SMT-LIB or Alloy (non-overlapping routing) and checks it. The translator's correctness is mechanically validated by the universal translate_soundness_standalone theorem in proofs/isabelle/SpecRest/soundness/DirectSound.thy. The compile command treats verify as a hard gate (--ignore-verify to bypass).
4. Convention map. The convention engine applies M1-M10 operation-classification rules; user-supplied conventions { ... } overrides win where present. See Convention Engine.
5. Emit. Handlebars templates produce the FastAPI project: app/, db/, alembic/, tests/, Dockerfile, docker-compose.yml, openapi.yaml, .github/workflows/ci.yml, Makefile, pyproject.toml.
6. Testgen (default; opt out with --no-tests). Adds a conformance suite under tests/ derived from the same requires/ensures/invariant clauses, rendered in the target's native language behind the Backend.scala seam (single shared derivation, pluggable ExprBackend/StrategyBackend/HarnessTemplates); the Python rendering is the byte-identical differential oracle. Coverage and skip rates are asserted by SkipRateProbeTest; per-language rendering parity by BackendTest.

Internal representation

The IR is a Scala 3 ADT (sealed abstract classes + final case classes) extracted from Isabelle by Code_Target_Scala. The source-of-truth definitions live in proofs/isabelle/SpecRest/core/IR.thy and are extracted to modules/ir/src/main/scala/specrest/ir/generated/SpecRestGenerated.scala on every isabelle build SpecRest.

There is one expression datatype: expr, 27 constructors covering the full input language (BoolLitF, IntLitF, IdentifierF, BinaryOpF(op, l, r, span), UnaryOpF, QuantifierF, WithF, LambdaF, MapLiteralF, SetComprehensionF, and so on), mutually recursive with field_assign, map_entry, and quantifier_binding. The parser emits it and every consumer module reads it. Until #391 the repo carried a second, 23-constructor subset datatype plus a lower projection between the two; that twin pipeline is gone. The verified subset is now carved out by the extracted translator itself: translate :: String.literal list => expr => smt_term option (the first argument is the service's enum names) returns Some exactly on the subset the soundness theorem covers, and the extracted trustGlobal / trustRequires / trustEnabled / trustPreservation classifiers drive the per-check trust dimension from that same boundary. The capstone theorem is translate_soundness_standalone in proofs/isabelle/SpecRest/soundness/DirectSound.thy; see Isabelle proofs, session layout.

The top-level service_ir plus the *_decl sub-declarations (entity_decl, field_decl, operation_decl, invariant_decl, function_decl, predicate_decl, transition_decl, conventions_decl, state_decl, ...) carry the surrounding declaration shape; constructors keep a Full/F suffix (ServiceIRFull, FieldDeclFull, BoolLitF). Extracted case-class fields are positional letters (a, b, c, ...) since the extractor doesn't preserve English names, but named selector functions (svcName, svcOperations, fldName, ...) are extracted alongside, so hand-written code never needs the letter mapping.

The same IR feeds the verifier (Z3 + Alloy translators), the convention engine, the codegen, and the testgen. IR canonicalization shipped in #202; the one-IR collapse in #391.

Project layout

Each module is a separate sbt subproject with test isolation; sbt <module>/test runs one module's tests. Every public entry point in verify/ returns IO[Either[VerifyError, _]].

Effect system layer

Every IO-returning stage (parse, IR build, Z3/Alloy translation, backend check, top-level Consistency.runConsistencyChecks) composes via IO.flatMap, and the whole pipeline is one fiber tree rooted at CommandIOApp.main. Backends are acquired as Resource[IO, _] so finalizers run on success, failure, and cancellation alike. The --parallel flag maps to parTraverseN(n); --timeout is enforced natively inside each backend (Z3's timeout solver param; Alloy's Future.get(timeout, ...)). See Concurrency and Cancellation for the full model, JMH numbers, and the cancellation contract.

CI surface

Ten workflows live under .github/workflows/:

Roadmap status

For the project-level phase ledger, the per-program milestone history (M_CE.* / M_L.* / M5.* / M6.*), the verifier capability inventory, and the closed-not-planned decisions, see Roadmap. Architecture stays scoped to system design.