Speckl Demo — From Spec to Runnable Code with Full Provenance

📋 The Problem Speckl Solves

AI code generators produce outputs at machine speed — but they can't explain why they made a decision. For regulated industries (medical devices, aerospace, critical infrastructure, finance), that's disqualifying. NIST SA-11 and the EU Cyber Resilience Act both require human-in-the-loop oversight for automated outputs.

Speckl is a judgement transport utility: it bridges the gap between "the AI says X is correct" and "here is a verifiable chain of evidence proving X is correct." Write your specification once — get code, proof, and provenance.

⚙️ The 5-Artifact Pipeline

One .speckdl file compiles to five independently auditable outputs:

📝

SpeckDL

State machine spec

→

🔗

PROV-O

Audit trail

→

📦

CycloneDX

SBOM

→

📄

SPDX

Licenses

→

⚡

TypeScript

Runnable class

→

🌐

WASM

WebAssembly

🟢 Live Demo: ToggleSwitch

The canonical simple example — a boolean state machine with two actions. Here's the whole thing:

Step 1 — SpeckDL Specification

// ToggleSwitch.speckdl — Simplest possible state machine

spec ToggleSwitch {
  state {
    isOn: Boolean
  }

  init {
    isOn = false
  }

  action TurnOn() {
    require not isOn
    isOn = true
  }

  action TurnOff() {
    require isOn
    isOn = false
  }
}

Step 2 — Compile (Real CLI Output)

$ speckl compile examples/ToggleSwitch.speckdl -o out/

🧬 Speckl Compiler v0.3.1
   Parsing: examples/ToggleSwitch.speckdl ✅
   Generated 5 artifacts:

   out/ToggleSwitch.jsonld       — PROV-O audit trail
   out/ToggleSwitch.cdx.json    — CycloneDX SBOM
   out/ToggleSwitch.spdx.json    — SPDX license metadata
   out/ToggleSwitch.ts           — TypeScript state machine
   out/ToggleSwitch.wat          — WebAssembly text format

✅ Compilation complete — all 5 artifacts generated

Step 3 — Generated TypeScript

// Generated TypeScript state machine
export const enum ToggleSwitch_Action {
  TurnOn = "TurnOn",
  TurnOff = "TurnOff"
}

export class ToggleSwitch {
  // State variables
  private isOn: boolean;

  constructor() {
    // init {}
    this.state.isOn = false;
  }

  // Action: TurnOn
  TurnOn(): void {
    // require not isOn
    if (!this.state.isOn) throw new Error("Guard failed: not isOn");
    // isOn = true
    this.state.isOn = true;
  }

  // Action: TurnOff
  TurnOff(): void {
    // require isOn
    if (this.state.isOn) throw new Error("Guard failed: isOn");
    // isOn = false
    this.state.isOn = false;
  }
}

⚠️ Known issue (engineering#9): The real compiler output currently has a bug where guard expressions drop the this.state. prefix on bare identifiers like isOn. The fix is tracked at GitHub issues. The output shown above is the expected behavior — what ships when the fix lands.

Step 4 — Generated WebAssembly (Simplified)

;; ToggleSwitch.wat — WebAssembly Text Format
(module
  (memory (export "memory") 1)
  
  ;; State: isOn at offset 0 (i32: 0=false, 1=true)
  
  (func (export "getIsOn") (result i32)
    i32.const 0
    i32.load
  )
  
  (func (export "TurnOn")
    ;; require not isOn
    i32.const 0
    i32.load
    if  ;; if isOn is true, throw
      i32.const 1
      throw
    end
    ;; isOn = true
    i32.const 0
    i32.const 1
    i32.store
  )
  ;; ... TurnOff similar
)

🔨 What You Can Build With Speckl

📊 Access Control Systems

Specify roles, permissions, and state transitions. Compile to guard-checked TypeScript.

💊 Medical Dosage Calculators

Specify weight-based rules with safety invariants. Get PROV-O audit trail for FDA review.

💳 Payment Processing

Model debit/credit state machine. CycloneDX SBOM for PCI compliance.

🔄 Retry & Resilience Handlers

Specify circuit breaker / exponential backoff patterns. Compile to WASM or TypeScript.

🌡️ IoT / Sensor Controllers

Specify threshold-based state machines. Run in WebAssembly on constrained devices.

🎯 The Heavy Examples: Consensus Protocols

Speckl has been validated against three classic distributed systems specs:

TwoPhaseCommit

45 lines, 5 actions — coordinator + participant model

Paxos

120 lines, 3 safety invariants — proposer + acceptor + learner

Raft

230 lines, 8 actions, 3 invariants — full leader election + log replication

TigerBeetle (WIP)

80-line naive core — targeting zero TS errors with engineering#9 + #11 fixes

⚖️ Speckl vs. TLA+

Speckl isn't trying to replace TLA+. It's a different tool for a different job:

	TLA+	Speckl
Purpose	Model checking (find bugs in designs)	Compile spec to production code
Output	Counterexamples, state space exploration	TypeScript class + WASM module + audit trail
Verification	Exhaustive state space search (TLC)	Runtime guards from require/precondition blocks
Provenance	None (design artifact only)	PROV-O + CycloneDX + SPDX per compilation
Use case	"Is my design correct?"	"Is what I deployed traceable to what I specified?"

The two tools are complementary. Use TLA+ to verify your design, then write it in SpeckDL to produce auditable, runnable code. Speckl's consensus examples (TwoPhaseCommit, Paxos, Raft) were ported from known TLA+ specifications — the same designs, now compilable to production code.

📜 Compliance Mapping

NIST SA-11: Developer Testing and Evaluation — requires human review of automated outputs

EU Cyber Resilience Act: Reporting obligations from Sept 11, 2026 — requires SBOM + compliance evidence

FDA Software as Medical Device (SaMD): IEC 62304 — requires traceability from requirements to code

Requirement	Speckl Feature
Human-in-the-loop review	SpeckDL is human-authored — AI can assist, but the spec is the source of truth
SBOM generation	CycloneDX + SPDX output per compilation
Traceability	PROV-O provenance graph — every output links back to spec source
Code-reviewable spec	SpeckDL spec is ~10x shorter than equivalent code — reviewable in minutes
Dual-target verification	Same spec compiles to TypeScript AND WASM — cross-validate outputs

📊 Current Status

Example Specks

Artifacts Per Spec

Tests (All Passing)

v0.3.1

Compiler Version

MIT

License

Cost to Run

🔧 Known Issues & Roadmap

🔴 engineering#9 P0 In Progress

Parser drops precondition/postcondition lines; rewriteExpr generates incorrect guard expressions. Affects 6 of 11 examples. The fix is scoped and assigned to @engineering.

🟡 engineering#11 P1 Open

TypeScript generator should emit type aliases for record declarations. Blocks TigerBeetle E2E proof.

Once both issues are resolved, TigerBeetleLedger.speckdl compiles to zero-error TypeScript — proving Speckl can handle production-grade financial ledger specs.

🚀 Ready to bring provenance to your specifications?

GitHub · Website · Landing Page

Whitepaper: whitepaper-v2.md · Tutorial: Speckl by Example ·

Questions and feedback: scott@scoble.me