diff --git a/demo/index.html b/demo/index.html index d1aac8d..9dd2039 100644 --- a/demo/index.html +++ b/demo/index.html @@ -3,7 +3,7 @@ -Speckl Demo — Judgement Transport for AI-Generated Code +Speckl Demo — From Spec to Runnable Code with Full Provenance

🧬 Speckl

-
Judgement Transport for AI-Generated Code
-
Specify → Verify → Generate → Prove. Every artifact traceable to its origin.
+
From Spec to Runnable Code — With Full Provenance
+
Write a state machine spec in SpeckDL. Get TypeScript, WASM, and 3 audit artifacts. Every output traceable to its source.
-

📋 The Problem

+

📋 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), that's disqualifying. + 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 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. + 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 Pipeline

+

⚙️ The 5-Artifact Pipeline

+

One .speckdl file compiles to five independently auditable outputs:

📝
SpeckDL
-
Human-authored spec with constraints
-
-
→
-
-
🔍
-
Z3 Verify
-
SMT solver checks invariants
-
-
→
-
-
⚡
-
Codegen
-
TypeScript / Rust from verified spec
+
State machine spec
→
🔗
-
Provenance
-
Immutable trace from spec to code
+
PROV-O
+
Audit trail
+
+
→
+
+
📦
+
CycloneDX
+
SBOM
+
+
→
+
+
📄
+
SPDX
+
Licenses
+
+
→
+
+
⚡
+
TypeScript
+
Runnable class
+
+
→
+
+
🌐
+
WASM
+
WebAssembly
- +
-

🟢 Live Demo: RetryHandler

-

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

+

🟢 Live Demo: ToggleSwitch

+

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

-

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 } +

Step 1 — SpeckDL Specification

+
// ToggleSwitch.speckdl — Simplest possible state machine - // 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 +spec ToggleSwitch { + state { + isOn: Boolean + } - // Verification conditions - verify: always(implies(attempt > 1, delay > 0)) - verify: always(implies(attemptCount == maxRetries + 1, not success)) + init { + isOn = false + } - // Design provenance + traceability - derives from FaultHandler - satisfies RESILIENCE-REQ-01 - author: Scott Scoble - review: manual + action TurnOn() { + require not isOn + isOn = true + } + + action TurnOff() { + require isOn + isOn = false + } }
-

Step 2 — Agent Output (Run Live)

-
$ speckl run RetryHandler.speck +

Step 2 — Compile (Real CLI Output)

+
$ speckl compile examples/ToggleSwitch.speck -o out/ -🧬 Processing Speck: RetryHandler - Constraints: 8 - Verify conditions: 2 +🧬 Speckl Compiler v0.3.1 + Parsing: examples/ToggleSwitch.speck ✅ + Generated 5 artifacts: -┌─ Verification Phase ─────────────────────────┐ -│ Task task-1: success │ -│ Z3 result: sat │ -│ All constraints verified │ -└──────────────────────────────────────────────┘ + 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 -┌─ Codegen Phase ──────────────────────────────┐ -│ Task task-2: success │ -│ Generated typescript code (27 lines) │ -│ Interface + constraint guards emitted │ -└──────────────────────────────────────────────┘ +✅ Compilation complete — all 5 artifacts generated
-✅ Result: success | Duration: 1ms
- -

Step 3 — Generated TypeScript

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

Step 3 — Generated TypeScript

+
// Generated TypeScript state machine +export const enum ToggleSwitch_Action { + TurnOn = "TurnOn", + TurnOff = "TurnOff" } -export type RetryHandlerOutput = { - success: boolean; - finalResult: string; - attemptCount: number; - totalDelay: number; -}; +export class ToggleSwitch { + // State variables + private isOn: boolean; -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"); + 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; + } }
-

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. +
+ ⚠️ 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 + marcus/engineering#9. + 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

+
- +
-

🤖 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
+

⚖️ Speckl vs. TLA+

+

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
TLA+Speckl
PurposeModel checking (find bugs in designs)Compile spec to production code
OutputCounterexamples, state space explorationTypeScript class + WASM module + audit trail
VerificationExhaustive state space search (TLC)Runtime guards from require/precondition blocks
ProvenanceNone (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

-

Speckl maps directly to these requirements:

- - - - + + + + +
RequirementSpeckl Feature
Human-in-the-loop reviewmanual review flag + sign-off provenance
SBOM generationBOM block → CycloneDX / SPDX export
TraceabilityDark Provenance graph — every derivation recorded
Constraint verificationZ3 SMT solver — mathematical proof of correctness
Human-in-the-loop reviewSpeckDL is human-authored — AI can assist, but the spec is the source of truth
SBOM generationCycloneDX + SPDX output per compilation
TraceabilityPROV-O provenance graph — every output links back to spec source
Code-reviewable specSpeckDL spec is ~10x shorter than equivalent code — reviewable in minutes
Dual-target verificationSame spec compiles to TypeScript AND WASM — cross-validate outputs
@@ -346,25 +472,47 @@

📊 Current Status

-
5
Example Specks
-
3
Compilation Targets (PROV-O, CycloneDX, SPDX)
-
9
Validation Checks
-
v0.3
Validator CLI
+
11
Example Specks
+
5
Artifacts Per Spec
+
41
Tests (All Passing)
+
v0.3.1
Compiler Version
MIT
License
$0
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.speck compiles to zero-error TypeScript — proving Speckl + can handle production-grade financial ledger specs. +

+
+
-

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

+

🚀 Ready to bring provenance to your specifications?

- Open standard — github | - codeberg mirror | - speckl.scoble.me + Forgejo · + Codeberg Mirror · + Landing Page

- Consulting, pilots, and speaking: scott@scoble.me + Whitepaper: whitepaper-v2.md · + Tutorial: Speckl by Example · + Distribution: distribution-strategy.md +

+

+ Consulting, pilots, and questions: scott@scoble.me

@@ -372,7 +520,7 @@ diff --git a/landing/index.html b/landing/index.html index d413dc8..91c2f1b 100644 --- a/landing/index.html +++ b/landing/index.html @@ -250,7 +250,8 @@ Your specification is the source of truth. Speckl ensures what gets built — by humans or AI — stays faithful to what you specified. Compile state machine specs into auditable code with embedded provenance.

- Source → + Live Demo → + Source Whitepaper v2 Tutorial