Spec Language Reference

Overview

The spec language is a purpose-built DSL for describing REST service behavior formally. It combines ideas from Alloy (relational modeling), TLA+ (state machine semantics), and Dafny (pre/post conditions).

Looking for the design rationale (why these constructs, what was surveyed, how the type system was chosen)? See Spec Language Design.

The semantics on this page are English-prose. The matching formal denotational semantics ships in Semantics.thy (an eval mutual function block over the IR ADT), and the universal translator-soundness theorem closes in Soundness.thy with zero sorry over all 23 expression constructors. Production verify routes in-subset shapes through the Isabelle-extracted Scala translator at ir/generated/SpecRestGenerated.scala (#192). For the trust-chain framing, the 2026 prior-art survey, and milestone history, see Mechanically Verified Translator Soundness; issue #88 (decomposed into M_L.0-M_L.4 + the #170 global-proof umbrella) closed 2026-04-26, with the Isabelle/HOL pivot #193 sealing the production cutover.

The authoritative grammar lives at modules/parser/src/main/antlr4/Spec.g4; when in doubt, that file wins over this prose.

Core concepts

Services

A service is the top-level unit. Each service maps to one REST API.

service MyService {
  // entities, enums, type aliases, state, operations, invariants, conventions
}

Entities

Entities define the data model. Each entity maps to a database table and a REST resource. Field constraints attach via a where clause rather than a default-value =. Per-entity invariant: clauses constrain the entity's own fields.

entity Url {
  code: ShortCode
  target: String where isValidURI(value)
  click_count: Int where value >= 0

  invariant: click_count >= 0
}

Primitive types: String, Int, Bool, Float, DateTime, Duration, UUID. Collection constructors use [ ] (not < >): Set[T], Map[K, V], Seq[T], Option[T]. User-defined enum and entity names are also valid types. Type aliases (type ShortCode = String where ...) let you name a constrained primitive once and reuse it.

State

The state { ... } block declares the named, mutable fields the operations read and write. State fields can be scalars, sets, sequences, or relations (A -> [one|lone|some|set] B).

state {
  store:    ShortCode -> lone String
  metadata: ShortCode -> lone UrlMapping
  base_url: String
}

Inside requires / ensures, a bare state name (e.g. store) refers to the pre-state; a primed name (e.g. store') refers to the post-state, following the TLA+ convention. pre(e) is an explicit pre-state cast for sub-expressions inside an ensures clause.

Operations

Operations declare state transitions with pre/post conditions. There is no function-style signature; inputs and outputs go in their own clauses, and contract clauses use requires: / ensures: (with the colon).

operation Shorten {
  input:  url: String
  output: code: ShortCode

  requires:
    isValidURI(url)

  ensures:
    code not in pre(store)
    store' = pre(store) + {code -> url}
    metadata'[code].url = url
    metadata'[code].click_count = 0
}

input: and output: are optional comma-separated name: type lists. requires: lists preconditions; ensures: lists postconditions. Each takes one or more expressions, conjoined.

Invariants

Invariants are properties that must hold across all states. The body comes after a colon. There is no brace-block form. Invariants may be named or anonymous.

invariant unique_codes:
  all c1, c2 in dom(store) |
    store[c1] = store[c2] implies c1 = c2

Quantifiers use the keywords all, some, no, exists. Bindings can be membership (x in expr) or type-named (x: TypeName). The body is separated from the bindings by a pipe (|) rather than a colon. Logical operators are word-form: and, or, not, implies, iff. Comparison is single = (== is invalid); inequality is !=.

Functions and predicates

User-defined helpers reduce duplication and feed both the verifier (inlined into VCs) and testgen (rendered as Python functions).

function days_until(deadline: DateTime, now: DateTime): Duration =
  deadline - now

predicate is_active(u: User) =
  u.status = Status.Active and u.deleted_at = none

The standard preamble auto-injects two predicates so every spec can use them without declaring them: isValidURI(s: String) and isValidEmail(s: String). Recognized built-ins translate directly into Python and SMT-LIB: len, dom, ran, max, min, now, days, sum.

Structural lints

spec-to-rest check <file>.spec runs six solver-free structural lints over the IR after parsing succeeds. Each diagnostic carries a stable code; warnings allow exit 0, errors cause exit 1.

L01 is intentionally narrow: it only fires on literals whose class admits no operator overload (e.g., flag and 5, count + true, count > true). The DSL uses +/- for set/map union and diff and + for string concatenation, so arithmetic-on-collection mismatches are not flagged without full type inference. A future ticket may add a richer typechecker.

L04 is a syntactic over-approximation of the broader "ambiguous dispatch" question. It catches duplicate-operation authoring bugs (same input/output, same requires modulo top-level and ordering and redundant true literals). It deliberately does not flag subsumption cases like requires: true against requires: count > 0; those are common idioms in correct specs (the caller picks the operation by name; ambiguity only matters at the dispatch layer). A SAT-based overlap check on requires_A and requires_B is candidate work for verify and is tracked separately.

Test-generation coverage

spec-to-rest compile --with-tests walks each ensures/requires/invariant clause and translates it to a Python assertion. The translator covers every IR Expr constructor; no translator coverage gaps remain. Clauses that still emit a skip fall into one of three categories: (a) user errors in the spec, unbound identifier (typo), reserved-name binding, call to a function that's neither a built-in nor declared via function/predicate, wrong arity on a user-declared call; (b) Quantifier typed-bindings (Colon), which need type-name -> instance enumeration not yet wired; (c) parser-side gaps that surface as translation skips, currently the multi-clause let ... in body in ecommerce. Skipped clauses are recorded in tests/_testgen_skips.json and omitted from the generated tests rather than emitted as pytest.skip notes.

Empirical skip rates on the canonical fixtures (locked in SkipRateProbeTest): safe_counter, url_shortener, todo_list, edge_cases all 0.0%; ecommerce 2.6% (2 / 76, parser scope leak in multi-clause let ... in body); auth_service 15.0% (6 / 40, undeclared hash / recentFailedAttempts calls). See Test Generation pipeline for the full surface.

Convention overrides

Default REST/DB mappings are overridden in a service-wide conventions { ... } block (per-operation with clauses are not part of the grammar). Each rule has the shape Target.property [qualifier] = value, where qualifier is a string literal used by http_header and test_strategy.

conventions {
  Shorten.http_method         = "POST"
  Shorten.http_path           = "/shorten"
  Shorten.http_status_success = 201

  Resolve.http_method         = "GET"
  Resolve.http_path           = "/{code}"
  Resolve.http_status_success = 302
  Resolve.http_header "Location" = output.url

  UrlMapping.db_table = "url_mappings"
  UrlMapping.plural   = "url_mappings"
  ShortCode.strategy  = "tests.strategies_user:short_code"
}

Each property is valid against a specific target kind:

The strategy and test_strategy properties point testgen at user-supplied Hypothesis strategies. See Test Generation pipeline, Custom strategies for the integration with --with-tests and the --strict-strategies CI gate.

See Convention Engine for the full mapping rules.