Speckl Demo — Judgement Transport for AI-Generated Code

📋 The Problem

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), that's disqualifying. NIST SA-11 and the EU Cyber Resilience Act both require human-in-the-loop oversight for automated outputs.

Speckl is judgement transport: it bridges the gap between "the AI says X is correct" and "here is a verifiable chain of evidence proving X is correct." It's the compliance layer for AI-generated code.

⚙️ The Pipeline

📝

SpeckDL

Human-authored spec with constraints

→

🔍

Z3 Verify

SMT solver checks invariants

→

⚡

Codegen

TypeScript / Rust from verified spec

→

🔗

Provenance

Immutable trace from spec to code

🟢 Live Demo: RetryHandler

Here's a real Speck for an exponential-backoff retry handler, running through the reference agent.

Step 1 — SpeckDL Specification

// RetryHandler.speck — Exponential backoff with constraint verification
speck RetryHandler {
  input: { operation: Operation, maxRetries: Nat, initialDelay: Real }
  output: { success: Bool, attemptCount: Nat, totalDelay: Real }

  // Invariants — must always hold
  constraint: maxRetries <= 10
  constraint: initialDelay > 0
  constraint: totalDelay == sum(delays)
  constraint: totalDelay <= 30s
  constraint: backoff(delay(n)) == delay(n-1) * 2

  // Verification conditions
  verify: always(implies(attempt > 1, delay > 0))
  verify: always(implies(attemptCount == maxRetries + 1, not success))

  // Design provenance + traceability
  derives from FaultHandler
  satisfies RESILIENCE-REQ-01
  author: Scott Scoble
  review: manual
}

Step 2 — Agent Output (Run Live)

$ speckl run RetryHandler.speck

🧬 Processing Speck: RetryHandler
   Constraints: 8
   Verify conditions: 2

┌─ Verification Phase ─────────────────────────┐
│ Task task-1: success                           │
│   Z3 result: sat                              │
│   All constraints verified                     │
└──────────────────────────────────────────────┘

┌─ Codegen Phase ──────────────────────────────┐
│ Task task-2: success                           │
│   Generated typescript code (27 lines)            │
│   Interface + constraint guards emitted        │
└──────────────────────────────────────────────┘

✅ Result: success | Duration: 1ms

Step 3 — Generated TypeScript

/** Generated from Speck: RetryHandler */
export interface RetryHandlerInput {
  operation: Operation;
  maxRetries: number;
  initialDelay: number;
  maxDelay: number;
}

export type RetryHandlerOutput = {
  success: boolean;
  finalResult: string;
  attemptCount: number;
  totalDelay: number;
};

export function retryhandler(input: RetryHandlerInput): RetryHandlerOutput {
  // Constraint checks (runtime guards)
  // constraint: maxRetries <= 10
  // assert(maxRetries <= 10, "c1");
  // constraint: maxRetries >= 0
  // assert(maxRetries >= 0, "c2");
  // constraint: initialDelay > 0
  // assert(initialDelay > 0, "c3");
  // constraint: maxDelay >= initialDelay
  // assert(maxDelay >= initialDelay, "c4");
  // constraint: totalDelay == sum(delays)
  // assert(totalDelay == sum(delays), "c5");
  // constraint: totalDelay <= 30s
  // assert(totalDelay <= 30s, "c6");
  // constraint: backoff(delay(n)) == delay(n-1) * 2
  // assert(backoff(delay(n)) == delay(n-1) * 2, "c7");
  // constraint: delay(n) <= maxDelay
  // assert(delay(n) <= maxDelay, "c8");
  // Implementation — compiled from verified DST
  throw new Error("RetryHandler: implementation pending DST compilation");
}

Step 4 — Provenance Graph (Dark Provenance)

speck:RetryHandler → z3:task-1 verified_by Z3 4.12.5

speck:RetryHandler → code:task-2 generated_from speckl-codegen

Every derivation is recorded. Every artifact is traceable. This is your compliance audit trail.

🤖 Agent Architecture

┌─────────────────────────────────────────┐
│           Orchestrator                    │
│   Accepts Specks, decomposes tasks       │
└───────┬───────────────┬─────────────────┘
        │               │
┌───────▼───────┐ ┌─────▼─────────┐
│ Team Lead    │ │ Team Lead      │
│ Verification  │ │ Codegen         │
└───────┬───────┘ └─────┬─────────┘
        │               │
┌───────▼───────┐ ┌─────▼─────────┐
│ Z3 SME       │ │ TypeScript SME │
│ (verify)      │ │ (emit)          │
└───────────────┘ └────────────────┘

// Tiered agents with TillDone condition-based task tracking
// Every SME records provenance edges for full traceability

📜 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

Speckl maps directly to these requirements:

Requirement	Speckl Feature
Human-in-the-loop review	manual review flag + sign-off provenance
SBOM generation	BOM block → CycloneDX / SPDX export
Traceability	Dark Provenance graph — every derivation recorded
Constraint verification	Z3 SMT solver — mathematical proof of correctness

📊 Current Status

Example Specks

Compilation Targets (PROV-O, CycloneDX, SPDX)

Validation Checks

v0.3

Validator CLI

MIT

License

Cost to Run

🚀 Ready to bring compliance to your AI-generated code?

Open standard — github | codeberg mirror | speckl.scoble.me

Consulting, pilots, and speaking: scott@scoble.me