# 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): ```typescript 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 { return { ...this._state }; } } ``` The TypeScript generator also handles `forall` loops, `if` statements, `let` bindings, and compound types (Set → `Set`, Map → `Map`, 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 *[Section 4: PROV-O generation, provenance graph structure, audit trail semantics]* ## 5. Consensus Protocols in SpeckDL *[Section 5: Two-Phase Commit, Paxos, and Raft case studies with compilation results]* ## 6. Compliance and Supply Chain *[Section 6: NIST SA-11 alignment, SBOM automation, regulatory use cases]* ## 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-3 complete; 4-8 forthcoming.*