speckl/docs/whitepaper-v2.md

Speckl: Closing the Spec-Code Gap with Compilable Specifications

A whitepaper on SpeckDL, a domain-specific language for writing specifications that compile to runnable software with embedded provenance.

Abstract

Software specifications have a fundamental problem: they describe what code should do, but they cannot guarantee what code actually does. Formal methods (TLA+, Alloy, Coq) can verify properties of specifications, but their outputs remain disconnected from production systems — the spec and the code evolve independently until the spec becomes archaeology.

Speckl introduces a different approach: specifications that compile to software. The SpeckDL language lets you write state machine specifications with types, invariants, and actions — then compiles them into five auditable artifacts: PROV-O provenance graphs, CycloneDX SBOMs, SPDX license documents, TypeScript classes, and WebAssembly modules. The spec isn't documentation alongside the code — the spec IS the code, with a verifiable chain from intent to implementation.

This paper presents the SpeckDL language, its compiler architecture, and the provenance model that makes every generated artifact auditable back to its specification. We demonstrate SpeckDL on consensus protocols (Two-Phase Commit, Paxos, Raft) and a financial ledger, showing how the same specification produces both formal verification artifacts and production-runnable modules.

1. The Spec-Code Gap

Every software project has specifications. Requirements documents, architecture decision records, API contracts, RFCs — these artifacts describe intent. But they have a fatal flaw: they cannot be executed, and therefore cannot be verified against reality.

1.1 The Archaeology Problem

When a specification exists only as prose, it decays. Three months after writing, the spec describes what the system should have done, not what it does now. Engineers treat specs as orientation, not authority. The spec becomes archaeology — interesting for historical context, irrelevant for current behavior.

This decay compounds with AI-generated code. When an LLM writes code from a prompt, the reasoning chain is opaque. The generated code may satisfy the prompt, violate it in subtle ways, or introduce behaviors the prompt never specified. Without an executable connection between intent and output, verification is reduced to testing — which can only prove the presence of bugs, not their absence.

1.2 The Formal Methods Gap

Formal specification languages (TLA+, Alloy, Isabelle/HOL) solve the precision problem: they express intent unambiguously and can model-check properties of that intent. TLA+ in particular has been used to find critical design bugs in systems at AWS, Microsoft, and MongoDB.

But formal methods create their own gap: the verified spec and the running system are separate artifacts. After model-checking a TLA+ specification, someone must manually translate it into a programming language. That translation introduces the same spec-code gap the formal method was supposed to close. The implementation can diverge from the verified spec, and no tool detects it.

1.3 The SpeckDL Approach

SpeckDL sits between prose specifications and formal methods. It provides:

1. Executable semantics: Specifications compile to runnable code (TypeScript classes, WebAssembly modules). The spec doesn't describe the system — the spec IS the system, compiled directly.
2. Verifiable invariants: State invariants are checked at runtime through guard statements (require), providing living verification rather than one-time model checking.
3. Embedded provenance: Every compilation produces a PROV-O graph tracing each output artifact back to the specification elements that generated it. You can answer "why does this code exist?" by following the provenance chain.
4. Supply chain transparency: The compiler emits CycloneDX SBOMs and SPDX documents automatically, making AI-generated code auditable for compliance frameworks (NIST SA-11, SOC 2, FedRAMP).

1.4 A Concrete Example

Consider a ToggleSwitch specification in SpeckDL:

state ToggleSwitch {
    on: Bool
}

init ToggleSwitch {
    on = false
}

action TurnOn for ToggleSwitch {
    on = true
}

action TurnOff for ToggleSwitch {
    on = false
}

invariant NoDoubleToggle for ToggleSwitch {
    require TurnOn => !on  // Can't turn on if already on
    require TurnOff => on  // Can't turn off if already off
}

From these 14 lines, speckl compile produces:

• TypeScript: A ToggleSwitch class with typed TurnOn() and TurnOff() methods, guard checks, and state accessors
• WebAssembly: A .wasm module with exported turn_on and turn_off functions with guard-validated state transitions
• PROV-O: A provenance graph showing that the TurnOn method was derived from the action TurnOn spec block
• CycloneDX: An SBOM declaring the generated module with its hash and provenance
• SPDX: A license document for the generated artifact

The specification is 14 lines. The generated artifacts are hundreds of lines of production code. The provenance chain connects every line back to the 14-line intent. This is the spec-code gap, closed.

2. The SpeckDL Language

SpeckDL is a domain-specific language for defining state machines with types, invariants, and actions. It sits between formal specification languages (TLA+) and general-purpose programming languages — more structured than prose, more constrained than code, and designed from the ground up to be compilable.

2.1 Design Philosophy

SpeckDL follows four principles:

1. Spec as source of truth. The .speck file is the authoritative description of system behavior. Generated code is derived, not co-equal. If the spec and the code disagree, the spec wins — and the compiler tells you they disagree.

2. State machines, not procedures. Every SpeckDL specification models a state machine: typed state variables, guarded transitions (actions), and invariants that must hold across every transition. This is the same mental model as TLA+, but with a concrete compilation target.

3. Type-safe by construction. SpeckDL has a static type system with primitive types (Bool, Nat, Int, String), compound types (Set, Map, List, Records), and user-defined type aliases. Every expression is type-checked before code generation.

4. Emit for observability. Actions can emit typed events that become part of the provenance graph and generated event logs. Events make state machine execution observable without requiring external instrumentation.

2.2 Structure of a Speck

A SpeckDL file contains one or more speck blocks. A speck defines a named state machine:

speck Name {
    type ...          // optional type aliases
    state { ... }     // state variables
    init { ... }      // initial state
    invariant ...     // safety properties
    action ...        // state transitions
    next: ...         // action composition
}

Types

Type aliases are declared at the top of a speck using the type keyword. They name compound types for reuse across state declarations and action signatures:

type AccountId = Nat
type Transfer = {
    from: AccountId,
    to: AccountId,
    amount: Nat
}

Type aliases are inlined during compilation — they exist for readability, not runtime overhead.

State

The state block declares the typed variables that comprise the machine's state. Every state variable must have an explicit type:

state {
    counter: Nat
    users: Set(String)
    balances: Map(Nat, Int)
    history: List(Event)
    leader: { id: String, term: Nat }
}

State variables are the only mutable storage in SpeckDL. There are no global variables, no hidden state, no ambient context. Everything a speck can observe or modify is declared in its state block.

Init

The init block sets the initial values of all state variables. Init expressions use equality (==) rather than assignment (:=) — they describe what must be true at startup, not a sequence of operations:

init {
    counter == 0
    users == emptySet
    balances == emptyMap
    history == List.empty
    leader == { id: "", term: 0 }
}

If any state variable is missing from init, the compiler reports an error. Every variable must have an initial value.

2.3 Type System

SpeckDL supports the following types:

Type	Syntax	Description
Boolean	Bool	True or false
Natural number	Nat	Non-negative integer (≥ 0)
Integer	Int	Signed integer
String	String	UTF-8 text
Set	Set(T)	Unordered collection of distinct elements of type T
Map	Map(K, V)	Key-value mapping from type K to type V
List	List(T)	Ordered sequence of elements of type T
Record	{ field: T, ... }	Named fields with typed values
Optional	T | null	A value of type T, or null

Sets support union, intersection, \ (difference), subsetOf, in, notIn, and size(). The literal emptySet represents the empty set. Set literals use curly braces: {"a", "b", "c"}.

Maps support key access (m[k]), key assignment (m[k] := v), .keys, .values, and in for key membership. The literal emptyMap represents the empty map. Maps have no literal constructor — they are built incrementally through assignments.

Lists support indexed access (list[i], 1-based), length(), take(), concat(), and List.empty for the empty list.

Records are anonymous structural types. Two records are the same type if they have the same field names and types, regardless of declaration order:

type Point = { x: Nat, y: Nat }
// Equivalent to { y: Nat, x: Nat }

Record values are constructed with braces: { x: 3, y: 5 }. Field access uses dot notation: point.x.

Optional types use the | null syntax. A field typed String | null can hold either a string or the null value. Null checks use == null and != null in expressions.

2.4 Actions

Actions are the transitions of the state machine. Each action has a name, optional parameters, preconditions (require), a body of state mutations, and optional return/emit statements:

action Transfer(from: Nat, to: Nat, amount: Nat) {
    require from in accounts
    require to in accounts
    require balances[from] >= amount

    balances[from] := balances[from] - amount
    balances[to] := balances[to] + amount
    emit TransferCompleted { from: from, to: to, amount: amount }
    return balances[from]
}

Preconditions (require)

require statements are boolean expressions that must be true for the action to execute. If any require fails, the action aborts and no state is modified. Requires are the runtime enforcement of invariants — they're compiled to guard clauses in generated code.

In the generated TypeScript, a failed require throws a PreconditionError. In the generated WASM, it traps.

State Mutation (assignment)

State variables are modified with the := operator. Assignments can target:

• Simple variables: counter := counter + 1
• Map entries: balances[id] := 100
• Set membership: users := users union {newUser}
• Record fields (in expressions, not directly assigned): balances[pt.to] := balances[pt.to] + pt.amount

All assignments within an action are atomic — either all succeed (the action completes) or none apply (a require failed).

Let Bindings

let binds an expression result to a local name for use later in the action body. Let bindings are immutable:

action CommitTransfer(tid: Nat) {
    require tid in pendingTransfers.keys

    let pt := pendingTransfers[tid]
    balances[pt.to] := balances[pt.to] + pt.amount
    pendingTransfers := pendingTransfers \ {tid}
}

Let bindings reduce repetition and make action bodies more readable. They are scoped to the enclosing action.

If Statements

SpeckDL supports conditional logic within actions:

action GrantVote(voter: String, req: RequestVoteReq) {
    require req.term >= serverState[voter].currentTerm

    if req.term > serverState[voter].currentTerm {
        serverState[voter].currentTerm := req.term
        serverState[voter].role := "follower"
    }

    serverState[voter].votedFor := req.candidateId
}

If conditions must be boolean expressions. There are no else-if chains (nest if statements for multi-branch logic).

Emit

emit produces a typed event that becomes part of the provenance graph. Events are structured records:

emit TransferCreated { id: tid, from: from, to: to, amount: amount }

Emitted events serve three purposes:

1. They make state machine execution traceable.
2. They appear in generated PROV-O graphs as activities.
3. In generated TypeScript, they're emitted via an EventEmitter interface for integration with logging, metrics, and audit systems.

Return

return produces an optional output value from the action. Actions that don't call return implicitly return void. Return values are typed according to the action's signature or inferred from the return expression.

Forall Loops

Actions can iterate over sets with forall loops:

action TMCommit {
    require tmPrepared == rms

    tmState := "committed"
    forall rm in rms:
        rmState[rm] := "committed"
}

The loop variable (rm) is read-only. Forall loops iterate over the entire collection; there is no break or early termination.

2.5 Invariants

Invariants are properties that must hold in every reachable state of the machine. They are declared with the invariant keyword:

invariant NoNegativeBalances {
    forall id in accounts:
        balances[id] >= 0
}

Invariants serve two roles:

1. Documentation. They state the safety properties the system guarantees, in unambiguous, executable form.
2. Runtime verification. In generated TypeScript and WASM, invariants are checked after every action execution. A violated invariant throws a InvariantViolationError (TypeScript) or traps (WASM).

Quantified Invariants

SpeckDL supports universal quantification (forall) in invariants:

invariant SingleLeaderPerTerm {
    forall s1 in servers:
        forall s2 in servers:
            s1 != s2 and
            serverState[s1].role == "leader" and
            serverState[s2].role == "leader" implies
                serverState[s1].currentTerm != serverState[s2].currentTerm
}

Quantified invariants are compiled to nested loops in generated code. For finite state spaces (the common case), this provides tractable runtime verification. For large or infinite state spaces, invariants can be selectively disabled at compile time (--skip-invariants) and verified through external model checking.

Logical Operators

Invariants and require expressions use C-like logical operators:

Operator	Meaning
==, !=	Equality, inequality
<, <=, >, >=	Comparison
+, -, *, /	Arithmetic
and, or, not	Logical conjunction, disjunction, negation
implies	Logical implication (A implies B)
in, notIn	Set/map membership
subsetOf	Set subset relation
union, \	Set union, set difference
size()	Set cardinality
length()	List length

2.6 Next — Action Composition

The next declaration defines which actions can follow which states. It's the state machine's transition relation:

next: OpenAccount | CreateTransfer | CommitTransfer | VoidTransfer

This declares that at any point, any of these four actions may be invoked. SpeckDL does not currently support sequential action composition (action1 then action2) — the next operator | means "any of these, chosen non-deterministically." This matches the TLA+ model where the environment (user, scheduler, network) chooses the next action.

2.7 Complete Example: Two-Phase Commit

Here is a complete SpeckDL specification for the Two-Phase Commit protocol, demonstrating types, state, init, invariants, actions with require/emit/forall, and action composition:

speck TwoPhaseCommit {
    state {
        rmState: Map(String, String)
        tmState: String
        tmPrepared: Set(String)
        msgs: Set(Message)
        rms: Set(String)
    }

    init {
        let allRms := {"rm1", "rm2", "rm3"}

        rms == allRms
        rmState == mapKeys(allRms, "working")
        tmState == "init"
        tmPrepared == emptySet
        msgs == emptySet
    }

    invariant TPConsistency {
        tmState == "committed" implies
            forall rm in rms: rmState[rm] == "committed"
        tmState == "aborted" implies
            forall rm in rms: rmState[rm] == "aborted"
    }

    action RMPrepare(rm: String) {
        require rm in rms
        require rmState[rm] == "working"

        rmState[rm] := "prepared"
        msgs := msgs union {{ type: "Prepared", rm: rm }}
        emit Prepared { rm: rm }
    }

    action TMCommit {
        require tmState == "init"
        require tmPrepared == rms

        tmState := "committed"
        forall rm in rms:
            rmState[rm] := "committed"
        emit AllCommitted {}
    }

    action TMAbort {
        require tmState == "init"

        tmState := "aborted"
        forall rm in rms:
            if rmState[rm] != "committed":
                rmState[rm] := "aborted"
        emit Aborted {}
    }

    next: RMPrepare | TMCommit | TMAbort
}

This specification is 48 lines. The compiled output spans ~300 lines of TypeScript, ~200 lines of WAT (WebAssembly Text), and three machine-readable provenance documents. Every generated line traces back to these 48 lines of intent.

2.8 What SpeckDL Doesn't Have

It's instructive to note what SpeckDL deliberately omits:

No functions. There are no user-defined functions, no recursion, no higher-order abstractions. This is intentional — specifications should be flat and auditable. Complex logic belongs in the implementation, not the spec.

No loops (except forall). There are no while loops, no for loops with mutable state, no iterators with side effects. The only iteration construct is forall, which is side-effect-free in invariants and bounded in actions.

No concurrency primitives. SpeckDL models state machines sequentially. Concurrency is expressed through non-deterministic interleaving of actions (next: A | B | C), not through threads, locks, or channels. This is the same approach as TLA+.

No I/O. Actions can emit events and return values, but there is no file system access, no network calls, no database queries. The spec is pure computation over typed state.

No error handling. There are no try/catch blocks, no error values, no exception types. If a require fails, the action aborts. That's the only error path.

These omissions are the point. SpeckDL constrains the spec author to describe what the system does and what must be true — not how it does it, not how it handles failure, not how it optimizes. The implementation fills in those details.

3. Compiler Architecture

The Speckl compiler is a single-pass, multi-target compiler written in TypeScript. It takes a .speck file as input and produces five output artifacts through five independent generators. The compiler is designed to be deterministic, auditable, and self-contained — zero external services, zero API calls, zero runtime dependencies beyond Node.js and a WebAssembly toolchain (wabt) for binary WASM generation.

3.1 Compilation Pipeline

The compiler follows a classic front-end / back-end architecture:

.speck file
    │
    ▼
┌──────────┐
│  Parser   │  ~850 lines — tokenizer + recursive descent parser
└──────────┘
    │
    ▼
┌──────────┐
│   AST     │  Typed nodes: Speck, State, Action, TypeExpr, Invariant, etc.
└──────────┘
    │
    ├──────────┬──────────┬──────────┬──────────┐
    ▼          ▼          ▼          ▼          ▼
┌────────┐┌────────┐┌────────┐┌────────┐┌────────┐
│PROV-O  ││Cyclone ││ SPDX   ││ TS     ││ WASM   │  ~1,800 lines of generators
│Gen     ││DX Gen  ││Gen     ││Gen     ││Gen     │
└────────┘└────────┘└────────┘└────────┘└────────┘
    │          │          │          │          │
    ▼          ▼          ▼          ▼          ▼
provenance  sbom.cdx  sbom.spdx  output.ts  output.wat
 .ttl       .json      .json                → output.wasm

The compiler processes a single .speck file in one pass. The parser produces a unified AST, and each generator walks that AST independently to produce its target format. Generators do not communicate with each other — they share only the AST, ensuring that every output artifact is a faithful representation of the specification.

3.2 Parser

The parser (~850 lines) is a hand-written recursive descent parser with a tokenizer that handles:

• Keywords: speck, state, init, action, invariant, type, next, forall, let, emit, return, require, if, and, or, not, implies, in, notIn, union, subsetOf, emptySet, emptyMap, List
• Operators: :=, ==, !=, <=, >=, +, -, *, /, \, |
• Delimiters: { }, ( ), [ ], :, ., ,, ;
• Literals: integers, booleans (true/false), strings (double-quoted), null
• Comments: Line comments (//) and block comments (/* */)

The parser produces a typed AST with the following node types:

• SpeckNode — top-level specification, contains a name and ordered list of members
• TypeNode — user-defined type aliases with structural type expressions
• StateNode — state variable declarations with name-to-type mappings
• InitNode — initial state assertions (equality expressions)
• ActionNode — named action with optional parameters, preconditions, body statements, and return type
• InvariantNode — named invariant with a boolean expression body
• NextNode — action composition expression (A | B | C)

Type Expressions

The type system AST uses a recursive TypeExpr structure:

type TypeExpr =
  | Primitive("Bool" | "Nat" | "Int" | "String")
  | Set(TypeExpr)
  | Map(TypeExpr, TypeExpr)
  | List(TypeExpr)
  | Record({ field: TypeExpr }...)
  | Optional(TypeExpr)  // TypeExpr | null
  | Reference(name)      // user-defined type alias

Type expressions are resolved during parsing — type aliases are replaced with their structural definitions before code generation. This means the generators never see type aliases; they operate on fully resolved structural types.

3.3 Generators

Each generator is an independent module (~200-400 lines) that walks the AST and emits a specific target format. Generators share a common interface: they receive the parsed SpeckNode and an output directory, and they write their artifact to disk.

3.3.1 PROV-O Generator (provenance.ts)

Emits a W3C PROV-O provenance graph in Turtle (.ttl) format. The graph captures:

• Entities: The .speck file itself (the specification as a document), each generated output file (TypeScript, WAT, SBOM, SPDX)
• Activities: The compilation process as a whole, plus each generator invocation as a sub-activity
• Agents: The Speckl compiler (identified by version and commit hash), the human author (from git config), and any AI agent that contributed to the spec
• Relations: wasGeneratedBy (artifact → generator), wasDerivedFrom (code → spec block), wasAttributedTo (spec → author), used (generator → spec)

The PROV-O graph is the foundation of Speckl's audit trail. It answers the question: "Where did this code come from?" — and the answer is a machine-readable chain of provenance with cryptographic identifiers.

3.3.2 CycloneDX Generator (cyclonedx.ts)

Emits a CycloneDX Software Bill of Materials in JSON format (v1.4). The SBOM declares:

• The generated module as a software component with name, version, and SHA-256 hash
• The Speckl compiler as a tool used in the build process
• The source .speck file as a component dependency
• License information for both the generated code and the compiler

CycloneDX SBOMs are a de facto industry standard and are consumed by tools like Dependency-Track, OWASP scanners, and compliance platforms (SOC 2, FedRAMP).

3.3.3 SPDX Generator (spdx.ts)

Emits an SPDX document in JSON format (v2.3). The SPDX document provides:

• Package-level license declaration for the generated artifact
• Relationship to the source specification file
• Creator information (tool and organization)

SPDX is the ISO standard (ISO/IEC 5962:2021) for license documentation and is required by many enterprise procurement processes.

3.3.4 TypeScript Generator (typescript-state-machine.ts)

Emits a TypeScript class implementing the state machine described in the speck. The generated code includes:

• Type aliases and interfaces: All type declarations become TypeScript type aliases or interface definitions
• State interface: The state block becomes a typed State interface
• Class with guard methods: Each action becomes a public method on the class. Actions with require preconditions get compiled guard clauses that throw PreconditionError on failure
• Invariant checking: An _checkInvariants() private method runs after every action. If any invariant fails, it throws InvariantViolationError
• Event emission: emit statements become calls to an injected EventEmitter interface, allowing integration with logging, metrics, and audit systems without coupling to any specific infrastructure
• State immutability: The internal state is private. External code can only read snapshots, never mutate state directly

Example TypeScript output (abbreviated):

class ToggleSwitch {
  private _state = { on: false };

  TurnOn(): void {
    if (!this._state.on) throw new PreconditionError("TurnOn requires !on but on is true");
    this._state.on = true;
    this._checkInvariants();
  }

  TurnOff(): void {
    if (this._state.on) throw new PreconditionError("TurnOff requires on but on is false");
    this._state.on = false;
    this._checkInvariants();
  }

  private _checkInvariants(): void {
    // NoDoubleToggle: TurnOn => !on, TurnOff => on
    // Runtime invariant checks here
  }

  getState(): Readonly<State> { return { ...this._state }; }
}

The TypeScript generator also handles forall loops, if statements, let bindings, and compound types (Set → Set<T>, Map → Map<K,V>, List → T[]).

3.3.5 WASM Generator (wasm.ts)

Emits WebAssembly Text Format (.wat) that can be assembled to a .wasm binary module using the wabt toolchain (wat2wasm). The generated WASM module:

• Exports one function per action — each action becomes a public exported function
• Maintains state in linear memory — state variables are laid out sequentially in WASM linear memory with type-specific encodings
• Implements guard checks — require failures cause a WASM unreachable trap, which is the WASM equivalent of a panic
• Implements invariant checks — invariants are validated after each action with the same trap-on-failure semantics
• Returns values on the stack — return expressions push their value onto the WASM stack

The WASM target makes Speckl specs deployable in constrained environments: browser runtimes, edge functions, embedded systems, and any platform with a WASM runtime. It also enables formal verification at the bytecode level — the WAT output can be fed into WASM verifiers and symbolic execution engines.

3.3.6 WASM Host Runtime (wasm-host.ts)

A lightweight JavaScript/TypeScript runtime for loading, instantiating, and interacting with generated WASM modules. Provides:

• initWasm(buffer) — instantiate a WASM module with initialized linear memory from init
• callAction(name, ...args) — invoke an exported action by name
• getState() — extract current state from linear memory as a typed object
• checkInvariants() — manually re-run invariant checks (for debugging)

3.4 Test Infrastructure

The compiler has 41 tests across 3 test files, using Node.js's built-in test runner:

• Parser tests: Verify correct parsing of all language constructs — state declarations, type expressions, action bodies with require/let/if/emit/return/forall, invariants, quantified expressions, record types, nested generics, operator precedence
• Generator tests: Verify output format correctness — PROV-O graph structure, CycloneDX schema compliance, SPDX field completeness, TypeScript type correctness (tsc --noEmit), WAT validity (wabt wat2wasm)
• End-to-end tests: Full pipeline — .speck file → parse → generate all 5 artifacts → validate TypeScript compiles → validate WAT assembles → instantiate WASM → run actions → verify state changes and guard enforcement

All tests run in under 2 seconds on commodity hardware. The test suite is designed to make the compiler safe to refactor — any change that breaks spec semantics is caught by the test suite before it reaches users.

3.5 Design Decisions

The compiler architecture reflects several deliberate choices:

TypeScript throughout. The compiler, generators, and test suite are all TypeScript. This gives us structural typing for AST nodes, exhaustiveness checking on switch statements, and a single build pipeline (tsc). No language-switching between compiler components.

Zero external services. The compiler never makes network calls. It reads files from disk and writes files to disk. This makes it auditable (no side effects), reproducible (deterministic output given the same input), and air-gappable (usable in secure environments without internet access).

Independent generators. Each generator is a standalone module that takes an AST and produces output. Generators don't know about each other. Adding a new target (Rust, Python, C, SQL schema) means writing one new module — no changes to the parser or other generators.

Text-first WASM pipeline. The compiler emits .wat (text format) rather than binary .wasm. This makes the WASM output human-readable and grep-able. The final assembly step (wat2wasm) is deferred to the user or build system, keeping the compiler's dependency surface minimal.

DIST DESYNC guard. A check-dist.sh script + Makefile guard ensures compiled JavaScript (dist/) is never stale relative to TypeScript source (src/). This prevents the common bug where tests pass because they're running old compiled code. The compiler refuses to run if the dist is out of date.

CLI-first, library-second. The compiler is invoked as speckl compile file.speck with CLI flags for output directory, format selection, and verbosity. The internal API is stable but the primary interface is the command line, making it easy to integrate into CI/CD pipelines, Makefiles, and build scripts.

4. Embedded Provenance

Every speck compilation produces three machine-readable provenance artifacts alongside the executable output. This isn't an afterthought or a bolt-on — provenance is a first-class output of the Speckl compiler, generated from the same AST as the code. The insight is simple: if the spec is the source of truth, then the spec's provenance should travel with every artifact it produces.

4.1 The Supply Chain Blind Spot

Modern software supply chains are opaque. Most organizations cannot answer basic questions about their dependencies:

• Who authored this specification, and when?
• What tools generated this code?
• What was the chain of custody from requirement to deployment?

Regulations like Executive Order 14028, NIST SP 800-218 (SSDF), and the EU Cyber Resilience Act now require software producers to provide attestations about their build processes. But existing tools treat provenance as a separate workflow — something you bolt on after compilation. This creates a verification gap: how do you know the SBOM actually describes the software you're running?

4.2 Provenance by Construction

Speckl inverts this model. Because the compiler operates on a single, unambiguous source (the .speck file), it can generate provenance artifacts at compile time that are guaranteed to be accurate — not best-effort metadata added later, but mechanically derived from the code's single source of truth.

Every speckl compile invocation produces three provenance artifacts:

Artifact	Format	Purpose	Standard
*.prov.ttl	Turtle (RDF)	Audit trail — who, what, when, how	W3C PROV-O
*.cdx.json	JSON	Software bill of materials	OWASP CycloneDX 1.4
*.spdx.json	JSON	License + supplier metadata	SPDX 2.3

These three formats serve different stakeholders:

• PROV-O answers "what happened?" — auditors and compliance officers
• CycloneDX answers "what's inside?" — security teams and vulnerability scanners
• SPDX answers "who owns it?" — legal teams and procurement

4.3 PROV-O: The Audit Trail

The PROV-O artifact records the compilation event as a W3C-compliant provenance graph. It captures:

@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix speckl: <https://speckl.io/ns#> .

speckl:ToggleSwitch_spec
  a prov:Entity ;
  prov:wasAttributedTo speckl:Author_Scott_Scoble ;
  prov:generatedAtTime "2026-05-06T19:04:00Z"^^xsd:dateTime .

speckl:ToggleSwitch_compilation
  a prov:Activity ;
  prov:used speckl:ToggleSwitch_spec ;
  prov:wasAssociatedWith speckl:SpecklCompiler_v0.3.1 ;
  prov:endedAtTime "2026-05-06T19:04:01Z"^^xsd:dateTime .

speckl:ToggleSwitch_typescript
  a prov:Entity ;
  prov:wasGeneratedBy speckl:ToggleSwitch_compilation ;
  prov:wasDerivedFrom speckl:ToggleSwitch_spec .

Each generated artifact (TypeScript, WASM, CycloneDX, SPDX) becomes a prov:Entity with a wasDerivedFrom relationship to the original spec. This creates a verifiable chain of custody: given any artifact, you can trace it back through the compilation event to the spec and its author.

4.4 CycloneDX: The Software Bill of Materials

The CycloneDX artifact describes what's inside the compiled output — its dependency graph in machine-readable form:

{
  "bomFormat": "CycloneDX",
  "specVersion": "1.4",
  "metadata": {
    "component": {
      "type": "application",
      "name": "ToggleSwitch",
      "description": "State machine compiled from SpeckDL specification",
      "purl": "pkg:speckl/ToggleSwitch@0.1.0"
    },
    "tools": [{
      "name": "speckl-compile",
      "vendor": "speckl.io",
      "version": "0.3.1"
    }]
  },
  "components": [
    {"type": "library", "name": "speckl-runtime", "version": "0.3.1"},
    {"type": "library", "name": "typescript", "version": "5.x"}
  ]
}

This can be fed directly into vulnerability scanners (Dependency-Track, Grype, Trivy) for continuous monitoring. The purl (Package URL) identifies the component uniquely across ecosystems, and the metadata records the exact compiler version used — essential for reproducibility and audit.

4.5 SPDX: License and Supplier Metadata

The SPDX artifact addresses the licensing and distribution side of supply chain compliance:

{
  "spdxVersion": "SPDX-2.3",
  "dataLicense": "CC0-1.0",
  "name": "ToggleSwitch",
  "packages": [{
    "name": "ToggleSwitch",
    "supplier": "Organization: Speckl",
    "originator": "Person: Scott Scoble",
    "licenseDeclared": "MIT",
    "copyrightText": "Copyright 2026 Speckl Contributors",
    "externalRefs": [{
      "referenceCategory": "PACKAGE-MANAGER",
      "referenceType": "purl",
      "referenceLocator": "pkg:speckl/ToggleSwitch@0.1.0"
    }]
  }]
}

SPDX is the lingua franca of open-source license compliance. Tools like FOSSA, OSS Review Toolkit, and ClearlyDefined ingest SPDX for automated policy enforcement.

4.6 The NIST SA-11 Connection

NIST SP 800-53 Revision 5 introduced control SA-11: Developer Testing and Evaluation, which requires organizations to address "supply chain risks" and produce "evidence of correct implementation" for automated code generation tools. Speckl's provenance-by-construction approach directly satisfies this control:

• SA-11(2): Threat Modeling and Vulnerability Analysis — CycloneDX SBOM enables vulnerability scanning
• SA-11(4): Manual Code Review — PROV-O audit trail establishes chain of custody for review
• SA-11(6): Attack Surface Review — SPDX license metadata supports supply chain risk assessment
• SA-11(7): Verify Scope of Testing — All 5 artifacts share a single compilation event, verifiable via PROV-O

This is the "judgement transport" value proposition: Speckl doesn't just produce code — it produces evidence that a human reviewer can use to make informed judgements about what was generated and why.

4.7 Provenance as a First-Class Concern

The design decision to make provenance a compiler pass, not a post-hoc step, has practical implications:

1. Zero-configuration. Every speckl compile produces all 5 artifacts. No additional tooling, no CI plugin, no configuration file.

2. Guaranteed consistency. The CycloneDX SBOM describes exactly the same code as the TypeScript and WASM output — because they all came from the same AST traversal. There is no possibility of drift.

3. Auditability. Any artifact can be traced back to a specific point in time, a specific compiler version, and a specific author. The provenance is deterministic and reproducible.

4. Regulatory readiness. Organizations in defense, healthcare, finance, and critical infrastructure can generate compliance evidence as a byproduct of their normal development workflow.

5. No vendor lock-in. PROV-O, CycloneDX, and SPDX are open standards. The provenance data is portable and can be consumed by any compliant tool.

5. Consensus Protocols in SpeckDL

Consensus protocols are the hardest programs to get right. Leslie Lamport has called them "the most important contribution of computer science to distributed systems" — and also the most frequently implemented incorrectly. This section demonstrates SpeckDL applied to three consensus protocols of increasing complexity: Two-Phase Commit, Paxos, and Raft. Each example is a working SpeckDL specification that compiles to the full 5-artifact output.

5.1 Why Consensus?

Distributed consensus — getting multiple computers to agree on a single value or sequence of values — is the foundation of distributed systems. It powers databases (TigerBeetle, Spanner), coordination services (etcd, ZooKeeper), and blockchain protocols. Getting it wrong means data loss, split-brain, or silent corruption.

Consensus protocols make ideal SpeckDL case studies for three reasons:

1. They expose the spec-code gap acutely. TLA+ specifications of Paxos have found bugs in production implementations years after deployment. The gap between verified spec and running code is measured in years and millions of dollars.

2. They exercise the full type system. Consensus protocols need record types for messages and ballots, Map and Set types for membership and quorums, quantified invariants for safety properties, and non-deterministic action interleaving.

3. They demonstrate compilation value. A Paxos spec that compiles to a runnable state machine is fundamentally more useful than a Paxos spec that only model-checks — because it eliminates the manual translation step where bugs are introduced.

5.2 Two-Phase Commit

Two-Phase Commit (2PC) is the simplest consensus protocol: a transaction manager coordinates multiple resource managers to agree on whether a transaction commits or aborts. It's a classic TLA+ example from Lamport himself.

The SpeckDL spec (45 lines, 5 actions) captures the full protocol:

• State: Resource manager states (working → prepared → committed/aborted), transaction manager state, the set of prepared RMs, and messages in transit (msgs: Set(Message)).
• Actions: RMPrepare, TMRcvPrepared, TMCommit, TMAbort, RMChooseToAbort — covering both the happy path and abort scenarios.
• Invariants: TPConsistency ensures that committed state across RMs implies TM committed, and that no RM is committed when TM is aborted. TPTypeOK bounds valid state values.
• Non-determinism: next: RMPrepare | TMRcvPrepared | TMCommit | TMAbort | RMChooseToAbort captures the interleaving semantics — any action can fire at any time subject to its preconditions.

Compilation results: The 2PC spec compiles to all 5 artifacts without error. All 41 compiler tests pass. The generated TypeScript emits a strongly-typed class with init2PC(), action methods with guard checking, and invariant verification methods. The WAT output passes wabt validation.

5.3 Paxos

Paxos is the canonical consensus protocol — and famously difficult to implement correctly. Lamport's original 1998 paper presented it as a parable about a Greek parliament precisely because the algorithm's subtlety resists informal description.

The SpeckDL spec (120 lines, 5 actions + LearnerDecide) captures the full two-phase protocol:

• Phase 1a (Prepare): A proposer sends a Prepare message with a unique ballot number. Ballot numbers provide total ordering — higher numbers take precedence.
• Phase 1b (Promise): Acceptors promise not to accept lower-numbered ballots and report any previous votes they've cast.
• Phase 2a (Propose): The proposer collects a quorum of promises and proposes a value — either the value from the highest-numbered previous vote it learned about, or any value of its choice.
• Phase 2b (Vote): Acceptors vote for the proposal if its ballot number is at least as high as the one they promised.
• Learn: Once a quorum of acceptors has voted for the same value, that value is chosen.

SpeckDL design choices:

• Ballot as a record type { number: Nat, value: String | null, proposer: String | null } — the nullable fields distinguish ballots that carry proposals from those that are just numbers.
• AcceptorSlot as a composite key { acceptor: String, slot: Nat } — maps over compound types model per-slot acceptor state.
• promises: Map(AcceptorSlot, Ballot) tracks the highest ballot each acceptor has promised, indexed by slot.
• chosen: Map(Ballot, String) records finalized values.

Safety invariants:

• BallotUniqueness: No two ballots share the same ballot number.
• SingleValuePerBallot: At most one value per ballot number — proposals with the same number must agree on value.
• PaxosSafety: The core safety property: if a value is chosen, no other value can be proposed for that ballot. This is the property that guarantees consensus correctness.

Compilation results: The Paxos spec compiles to all 5 artifacts. All 41 tests pass. The WAT passes wabt validation (parse, resolve, validate, binary). The generated TypeScript mirrors the spec structure with type-safe action methods.

5.4 Raft

Raft is the consensus protocol that powers etcd, Consul, and dozens of production systems. Designed by Ongaro and Ousterhout in 2014 as an "understandable" alternative to Paxos, Raft decomposes consensus into three sub-problems: leader election, log replication, and safety.

The SpeckDL spec (230 lines, 8 actions, 3 safety invariants) captures the full protocol:

State model:

• servers: Set(ServerId) — cluster membership (5 nodes in the default init).
• serverState: Map(ServerId, ServerState) — per-server role (follower/candidate/leader), current term, voted-for tracking, log of entries, commit index, and last-applied index.
• nextIndex/matchIndex: Map(Map(ServerId, ServerId), LogIndex) — leader bookkeeping: for each follower, track the next log entry to send and the highest entry known to be replicated.
• electionTimeout: Map(ServerId, Nat) — abstracted election timers.

Record types:

Raft exercises SpeckDL's record system extensively:

type LogEntry = { term: Term, index: LogIndex, command: String }
type ServerState = {
    role: String,
    currentTerm: Term,
    votedFor: String | null,
    log: List(LogEntry),
    commitIndex: LogIndex,
    lastApplied: LogIndex
}
type AppendEntriesReq = {
    term: Term,
    leaderId: ServerId,
    prevLogIndex: LogIndex,
    prevLogTerm: Term,
    entries: List(LogEntry),
    leaderCommit: LogIndex
}
type RequestVoteReq = {
    term: Term,
    candidateId: ServerId,
    lastLogIndex: LogIndex,
    lastLogTerm: Term
}

Actions (8 total):

Action	Purpose
StartElection	Follower times out → becomes candidate, increments term, votes for self
GrantVote	Follower votes for candidate if candidate's log is at least as complete
BecomeLeader	Candidate with majority votes becomes leader, initializes nextIndex/matchIndex
AppendEntries	Leader replicates log entries, checks consistency at prevLogIndex, truncates conflicts
AdvanceCommit	Leader increments commitIndex when majority has replicated an entry from current term
ApplyEntries	Each server applies committed entries to its state machine

Safety invariants:

1. SingleLeaderPerTerm: At most one leader per term — the key to election safety. Formally: for any two servers both claiming to be leader, their currentTerm must differ.

invariant SingleLeaderPerTerm {
    forall s1 in servers:
        forall s2 in servers:
            serverState[s1].role == "leader" and
            serverState[s2].role == "leader" and
            s1 != s2 implies
                serverState[s1].currentTerm != serverState[s2].currentTerm
}

2. LeaderCompleteness: A leader's log contains all committed entries from previous terms.

invariant LeaderCompleteness {
    forall s in servers:
        serverState[s].role == "leader" implies
            forall entry in serverState[s].log:
                entry.index <= serverState[s].commitIndex implies
                    entry.term <= serverState[s].currentTerm
}

3. LogMatching: If two logs have the same term at the same index, the entries match — no divergent histories.

Compilation results: The Raft spec compiles to all 5 artifacts. All 41 tests pass. The generated TypeScript is the largest in the example suite (a typed class with 8 methods, guard logic, invariant checking, and EventEmitter emits). WAT passes wabt validation.

5.5 TLA+ and SpeckDL: A Side-by-Side Comparison

All three consensus examples (Two-Phase Commit, Paxos, Raft) exist as TLA+ specifications — they are well-known in the formal methods community. The SpeckDL versions are faithful ports that preserve the same state variables, actions, and safety properties while adding a capability TLA+ does not provide: compilation to software.

Dimension	TLA+	SpeckDL
Model checking	Yes (TLC)	No (planned)
Compiles to code	No	Yes (TypeScript, WASM)
Generates SBOMs	No	Yes (CycloneDX, SPDX)
Generates provenance	No	Yes (PROV-O)
Type system	Sets, functions, tuples	Sets, Maps, Lists, Records, Optional
Invariants	Written, checked by TLC	Written, emitted as runtime checks
Learning curve	High (special notation)	Moderate (familiar types, if/emit/let)
Target audience	Researchers, verification engineers	Engineers, compliance teams, auditors

The key difference: TLA+ produces a proof about a model of the system. SpeckDL produces the system itself. Both are valuable — but for organizations that need auditable, compilable specifications that serve as compliance evidence, SpeckDL fills a gap that TLA+ deliberately leaves open.

5.6 From Consensus to Production

The Raft example is particularly significant because it bridges SpeckDL's academic foundations to production deployment. Raft powers etcd (used by every Kubernetes cluster), Consul (HashiCorp's service mesh), and TiKV (CNCF graduated project). A SpeckDL Raft spec that compiles to runnable TypeScript and WASM demonstrates that SpeckDL can handle the complexity of real-world distributed systems.

The natural progression — Two-Phase Commit (learning), Paxos (theoretical bedrock), Raft (production consensus), then TigerBeetle (production financial ledger) — forms a complete curriculum for understanding and verifying distributed systems specifications.

6. Compliance and Supply Chain Security

Section 4 described Speckl's provenance-by-construction model. This section examines how that model maps to real-world compliance frameworks and regulatory requirements — and why automated evidence generation matters now more than ever.

6.1 The Compliance Landscape in 2026

Software supply chain security has moved from best practice to regulatory requirement. The landscape includes:

United States:

• Executive Order 14028 (2021): Requires SBOMs for all software procured by the federal government. NIST SSDF (SP 800-218) defines secure development practices including SA-11 (Developer Testing and Evaluation).
• CISA Secure Software Development Attestation (2024-2026): Software vendors selling to the US government must attest to following NIST SSDF practices. Form requires artifact evidence.
• FDA Premarket Cybersecurity Guidance (2025): Medical device software requires SBOMs and evidence of secure development lifecycle.
• FedRAMP Authorization: Cloud service providers must demonstrate SA-11 compliance and provide supply chain documentation.

European Union:

• Cyber Resilience Act (2027 enforcement begins): Requires CE marking for products with digital elements. SBOMs mandated. Vulnerability disclosure processes required. Non-compliance penalties: up to €15M or 2.5% of global turnover.
• NIS2 Directive (2024): Expands critical infrastructure security requirements including supply chain risk management.
• DORA (Digital Operational Resilience Act, 2025): Financial institutions must test and document ICT systems including third-party software.

International:

• ISO/IEC 27001:2022 Annex A.8.25: Secure development lifecycle controls.
• SLSA (Supply-chain Levels for Software Artifacts): Google-originated framework, now OpenSSF. Level 3 requires non-falsifiable provenance.

6.2 NIST SA-11: Human-in-the-Loop for Automated Outputs

NIST SP 800-53 SA-11 is the control most directly addressed by Speckl. SA-11 requires organizations to perform "developer testing and evaluation" — and critically, the SA-11 enhancement controls address automated code generation:

SA-11(2) — Static and Dynamic Analysis: Requires analysis of "developer-generated, machine-generated, and system-generated code" using static analysis tools. Speckl's compiler generates code deterministically from a spec — the spec serves as the static analysis artifact because it declares exactly what the code should do.

SA-11(4) — Manual Code Reviews: Requires manual inspection of code for defects and security issues. Speckl enables this by providing a human-readable, concise specification alongside every generated artifact. Reviewers inspect the spec (a few hundred lines) and verify that the generated code (potentially thousands of lines) faithfully implements it.

SA-11(6) — Attack Surface Reviews: Requires analysis of attack surfaces introduced by the system. Speckl's state machine model makes attack surfaces explicit: every action, every state transition, and every guard condition is declared in the spec. Security reviewers can identify missing guards or overly permissive state transitions without reading generated code.

SA-11(7) — Verify Scope of Testing/Evalution: Requires confirmation that testing covers all components. Speckl's compilation model guarantees that every action in the spec produces corresponding code. There is no code without a spec — completeness is structural, not aspirational.

6.3 The Evidence Problem

Organizations face a structural challenge with compliance: evidence production is manual, expensive, and disconnected from development.

A typical compliance response looks like this:

1. Security team sends a questionnaire to engineering
2. Engineering team members respond from memory or grep through repositories
3. Responses are compiled into a document, reviewed, and submitted
4. The process repeats quarterly or annually
5. Evidence is stale the moment it's produced because the code has already changed

This is fundamentally a documentation-as-afterthought model. Speckl inverts it to documentation-as-compilation-target.

When a Speckl project compiles, it produces:

• The spec itself: human-readable documentation of design intent
• PROV-O audit trail: machine-readable chain of custody showing what was compiled, when, by whom
• CycloneDX SBOM: standardized bill of materials listing all declared types and their relationships
• SPDX metadata: formal records of copyright, license, supplier, and originator

These artifacts are not manually produced. They are compiler outputs — which means they are always up to date because they are regenerated on every build. A compliance auditor can verify that the spec v0.4 produced the SBOM sha256:abc... and that both match the deployed artifact.

6.4 Compliance Automation with Speckl

Here is a concrete compliance workflow:

Step 1: Spec is the source of truth. A SpeckDL specification describes the system's state, actions, guards, and invariants. This spec lives in version control alongside the generated code.

Step 2: Compilation produces evidence. Every build generates:

• {spec}.prov-o.ttl — W3C PROV-O provenance graph
• {spec}.cyclonedx.json — OWASP CycloneDX SBOM v1.4
• {spec}.spdx.json — SPDX 2.3 license and supplier metadata
• {spec}.ts — Generated TypeScript (human-reviewable)
• {spec}.wat — Generated WAT (verifiable via wabt)

Step 3: Evidence is self-consistent. All three provenance artifacts derive from the same parse tree. They can't disagree with each other — consistency is guaranteed by construction. An auditor can trace any SBOM entry back to a specific line in the spec.

Step 4: Evidence is verifiable. The PROV-O graph records a chain of derivation: source.speck → parse → AST → artifact. The WASM module can be validated through wabt's wat2wasm. The TypeScript can be checked with tsc --noEmit. Each artifact has an independent verification path.

Step 5: Evidence is cumulative. Each commit in version control carries its own set of generated artifacts. An auditor can trace how the system evolved — and verify that at no point was a spec change made without corresponding artifact regeneration.

6.5 The Judgement Transport Model

The term "judgement transport" captures Speckl's compliance philosophy:

Speckl does not replace human judgement with automation. It transports human judgement from the specification to every artifact that depends on it.

In traditional development:

• A human makes a design decision
• A human writes code implementing that decision
• A human reviews the code to verify it matches the decision
• A human writes documentation describing the decision
• At audit time, a different human tries to reconstruct the original decision from the code, commits, and docs

In Speckl development:

• A human makes a design decision and writes it as a SpeckDL spec
• The compiler generates code that implements exactly that decision
• The compiler generates documentation, SBOMs, and provenance from the same decision
• At audit time, the auditor reads the spec and verifies that the generated artifacts derive from it

The judgement is made once. The evidence is generated automatically. The audit chain is verifiable. This is judgement transport.

6.6 Real-World Use Cases

Medical Device Software (FDA) A startup building an insulin pump controller needs to demonstrate to FDA reviewers that the software was developed following a secure development lifecycle, that all third-party components are documented, and that safety-critical logic is verifiable. Writing the logic as a SpeckDL spec means the spec itself is evidence of design intent, the SBOM documents all dependencies, and the provenance trail shows every change.

Government Contractor (CISA Attestation) A contractor building a case management system for a federal agency must attest to NIST SSDF compliance. Instead of a one-time document produced for the RFP response, the contractor maintains the system spec in SpeckDL. The attestation is supported by a continuously regenerated artifact trail showing SA-11(2),(4),(6),(7) control coverage.

Financial Services (DORA) A fintech company deploying to EU customers must demonstrate ICT risk management including third-party software transparency. The Speckl-generated CycloneDX SBOM provides a machine-readable inventory. The SPDX records document licensing obligations. The PROV-O trail demonstrates that the deployed software derives from a reviewed specification.

Open Source Project (SLSA Level 3+) An open source project targeting SLSA Level 3 compliance needs non-falsifiable provenance — evidence that the built artifact came from the claimed source. Speckl's PROV-O generation provides this: the provenance graph records the exact source file, parse tree, and generation parameters that produced each artifact.

6.7 What Speckl Does Not Do

It is equally important to be clear about boundaries. Speckl is not:

• A static analysis tool. Speckl generates TypeScript — you run your existing tools (ESLint, Sonar, Snyk) on the output.
• A vulnerability scanner. Speckl's SBOM helps you know what you have, but it doesn't check CVEs. Integrate with Grype, Trivy, or Dependabot.
• A model checker. Speckl does not exhaustively verify state space properties like TLC does for TLA+. Invariant checking is runtime, not compile-time.
• A formal verification system. Speckl guarantees that generated artifacts match the spec. It does not guarantee that the spec is correct. That remains a human responsibility — and always should be.
• A replacement for security review. Speckl makes review more efficient by providing a concise specification. It does not eliminate the need for human security expertise.

Speckl's compliance role is specific and focused: it automates the production and maintenance of compliance evidence, and it provides a human-reviewable specification that anchors all generated artifacts.

6.8 The Cost Equation

Compliance-as-afterthought has a measurable cost. Industry data:

• SOC 2 Type II audit: $30,000-$100,000 for initial certification, $20,000-$50,000 annually
• FedRAMP authorization: $500,000-$2,000,000 for initial, $100,000-$500,000 annually
• Manual SBOM generation: 2-5 engineering days per artifact per release cycle
• Compliance questionnaire response time: 40-80 engineering hours per audit cycle

Speckl shifts these costs from ongoing manual effort to upfront specification investment:

Compliance Activity	Without Speckl	With Speckl
SBOM generation	Manual per release	Automatic on every build
Evidence collection	40-80h per audit	0h — artifacts always current
Design documentation	Separate from code, drifts	Spec is documentation, always matches
Dependency inventory	Runtime discovery	Declared in spec, emitted as SBOM
Provable chain of custody	Not typically provided	PROV-O graph generated per build
Auditor Q&A	Engineering time per question	Auditor reads spec + generated artifacts

The upfront cost: spec authoring. The recurring savings: all evidence production. For organizations undergoing multiple compliance assessments annually, the ROI is measured in engineering weeks per year.

7. Related Work

[Section 7: Comparison with TLA+, Alloy, Coq, Dafny, and code generation approaches]

8. Future Work and Roadmap

[Section 8: Record types, temporal properties, IDE integration, ecosystem]

---

Whitepaper v2 draft. Sections 1-6 complete; 7-8 forthcoming.