diff --git a/demo/index.html b/demo/index.html new file mode 100644 index 0000000..d1aac8d --- /dev/null +++ b/demo/index.html @@ -0,0 +1,379 @@ + + + + + +Speckl Demo — Judgement Transport for AI-Generated Code + + + + +
+

🧬 Speckl

+
Judgement Transport for AI-Generated Code
+
Specify → Verify → Generate → Prove. Every artifact traceable to its origin.
+
+ +
+ + +
+

📋 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:

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

📊 Current Status

+
+
5
Example Specks
+
3
Compilation Targets (PROV-O, CycloneDX, SPDX)
+
9
Validation Checks
+
v0.3
Validator CLI
+
MIT
License
+
$0
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 +

+
+ +
+ + + + +