spec_to_rest

A compiler that proves your REST service satisfies its specification before emitting code. The toolchain is Scala 3, Cats Effect 3, Z3, and Alloy; translator soundness is mechanically checked in Isabelle/HOL.

You write the spec: entities, operations with pre/post-conditions, invariants. spec-to-rest verify discharges the proof obligations against Z3 and Alloy. spec-to-rest compile emits nothing when any check fails. When it passes, the emitter writes a complete service for any of three target stacks (Python/ FastAPI, Go/chi, TypeScript/Express) across Postgres, SQLite, or MySQL. --with-tests adds a conformance suite in that target's own language (pytest+Hypothesis, Vitest+fast-check, or go test+rapid), single-sourced from the same spec.

Source is on GitHub. The spec language reference covers syntax; the verification pipeline page covers solver routing.

Spec -> Verify -> Emit

A trimmed view of fixtures/spec/url_shortener.spec, the verifier's check list, and an excerpt of the FastAPI router emitted for the Python target (chi and Express render the same spec into their own stacks), all from one compile invocation:

service UrlShortener {
type ShortCode = String where
  len(value) >= 6 and len(value) <= 10

entity UrlMapping {
  code: ShortCode
  url: String where isValidURI(value)
  click_count: Int where value >= 0
}

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

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

  requires: isValidURI(url)
  ensures:
    code not in pre(store)
    store' = pre(store) + {code -> url}
}

invariant metadataConsistent:
  dom(store) = dom(metadata)
}

from fastapi import APIRouter, Depends, HTTPException
from sqlalchemy.ext.asyncio import AsyncSession

from app.database import get_session
from app.schemas.url_mapping import (
  ShortenRequest,
  UrlMappingRead,
)
from app.services.url_mapping import UrlMappingService

router = APIRouter(tags=["url_mapping"])


@router.post("/shorten", status_code=201)
async def shorten(
  body: ShortenRequest,
  session: AsyncSession = Depends(get_session),
) -> UrlMappingRead:
  svc = UrlMappingService(session)
  return await svc.shorten(body)


@router.get("/{code}", status_code=200)
async def resolve(
  code: str,
  session: AsyncSession = Depends(get_session),
) -> UrlMappingRead:
  svc = UrlMappingService(session)
  result = await svc.resolve(code)
  if result is None:
      raise HTTPException(status_code=404, detail="not found")
  return result

If any check above had returned unsat, compile would exit non-zero and write nothing, not even an empty output directory. See Verify-as-gate in compile.

What is a verifying compiler?

Most code generators are scaffolds: they write boilerplate from a schema, then trust you to keep the runtime correct. A verifying compiler treats the specification as a logical theory. Each operation produces a verification condition (VC), a first-order formula that must be unsatisfiable for the operation to preserve every invariant. The compiler discharges those VCs against an SMT solver, and only emits code once every check has been mechanically discharged. The guarantee: on every input the specification admits, the generated handlers leave every invariant intact.

How spec_to_rest compares

Behind the compiler

Five stages run on every invocation: Parse (ANTLR4) -> IR Build -> Verify (Z3 + Alloy) -> Map (M1-M10 conventions) -> Emit (Handlebars). Each stage returns IO; failures land in Either[VerifyError, _].

A static classifier routes each proof obligation to the solver that fits. Z3 owns first-order invariants and preservation; Alloy owns powerset (^) and always/eventually. The two coverage areas do not overlap.

Per-check timeouts run inside the solver. SIGINT propagates through fiber cancel to Z3 Context.interrupt(). --parallel n dispatches via parTraverseN.

When verify succeeds, compile emits the full project for the chosen target: source tree, migrations, openapi.yaml, Dockerfile, docker-compose.yml, and a CI workflow (the FastAPI layout is app/ + alembic/; chi and Express emit their own idiomatic trees). When verify fails, each failing check is rendered in prose: which operation, which invariant, which contributing field, with concrete pre and post values lifted from the solver model.

--dump-vc <dir> writes per-check .smt2 and .als files alongside verdicts.json. --explain extracts the Z3 unsat core and surfaces the contributing spec spans. The translator's correctness is mechanically validated by a universal soundness theorem in proofs/isabelle/SpecRest/Soundness.thy.