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 the spec language foundations.

The semantics on this page are English-prose. The matching formal denotational semantics ships in Semantics_Reference.thy (an eval mutual function block over the IR ADT), and the universal translator-soundness theorem (translate_soundness_standalone) closes in DirectSound.thy with zero sorry over the verified subset. Production verify routes in-subset shapes through the Isabelle-extracted Scala translator at modules/ir/src/main/scala/specrest/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.

Security schemes

A service-wide security { ... } block declares named credential schemes; an operation opts in with a requires_auth: clause naming one or more of them.

security {
  bearer: Bearer(bearer_format: "JWT")
  api_key: ApiKey(header: "X-API-Key")
  basic: Basic
}

operation GetProfile {
  requires_auth: bearer, api_key

  output: profile: User

  ensures:
    true
}

Three scheme kinds exist. Bearer takes an optional bearer_format; ApiKey takes exactly one location argument (header, query, or cookie) whose value is the parameter name; Basic takes no arguments. A comma list in requires_auth: means the schemes are alternatives (a client may satisfy any one of them - OpenAPI security-array semantics). Operations without the clause are public. Referencing an undeclared scheme or declaring two schemes with the same name is a compile-time error.

Operation classification and verification ignore auth: it changes neither the CRUD/synthesis routing nor the state-machine invariants the proofs cover. Codegen does consume it. Declared schemes emit into OpenAPI securitySchemes (#54), and operations with requires_auth: are enforced by per-scheme Bearer/ApiKey/Basic guards in the generated FastAPI, Go/chi, and TS/Express services (#55).

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 (test emission is on by default; opt out with --no-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 60.0% (3 / 5), url_shortener 4.8% (1 / 21), todo_list 4.0% (2 / 50), edge_cases 10.3% (3 / 29) - all from unbacked scalar state the admin /state endpoint projects as null; ecommerce 6.6% (5 / 76, mostly unbacked-scalar + 2 from a parser scope leak); auth_service 9.8% (4 / 41, all unbacked scalar-state - hash, time-unit, and recentFailedAttempts builtins translate as of #307). 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 applies to a specific target kind.

Operation

Entity

Type alias / Enum

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

See Convention Engine for the full mapping rules.