From d6e8bf906a32386fae39d3a54524a165157a5ab8 Mon Sep 17 00:00:00 2001 From: Scott Scoble Date: Fri, 8 May 2026 09:11:48 -0700 Subject: [PATCH] landing: rewrite to match current Speckl reality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace 'dark provenance' / constraint-based / Z3 messaging with what Speckl actually does: state machine compilation to 5 auditable artifacts (PROV-O, CycloneDX, SPDX, TypeScript, WASM). Update code example from old 'speck' syntax to current 'spec' / state / init / action keywords. Add pipeline grid, real examples (TwoPhaseCommit, Paxos, Raft, Forgejo workflow), strategy ladder with completion status, quickstart section with real CLI commands. The old landing page described a completely different product — one that didn't exist. This version accurately reflects the compiler, examples, and whitepaper v2 that are actually built and working. --- landing/index.html | 469 +++++++++++++++++++++++++++++---------------- 1 file changed, 302 insertions(+), 167 deletions(-) diff --git a/landing/index.html b/landing/index.html index 3f576e1..d413dc8 100644 --- a/landing/index.html +++ b/landing/index.html @@ -3,26 +3,26 @@ - Speckl — Spec-First Development with Dark Provenance - + Speckl — A Judgement Transport Utility for AI-Generated Specifications + - - + + - @@ -199,111 +245,200 @@

Speckl

-

Where humans and AI collaborate in the same language.
Spec-first development with dark provenance. Write what your system should do. Prove it. Ship with full traceability.

+

A Judgement Transport Utility

+

+ 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 Code - Read the Whitepaper - + Source → + Whitepaper v2 + Tutorial
-

What is Speckl?

-

Speckl is an open standard for specification-first development with dark provenance. It defines how to write what a system should do — in a machine-verifiable format — before any code is written. Every behavior traces back to its source of intent.

- -

Speckl is not a product or a platform. It is a methodology and language specification, published freely under MIT. The SpeckDL language, the Dark Provenance methodology, and the reference implementations define the standard. Products built on it — compilers, verification tools, compliance APIs — will come as the ecosystem grows.

- -
-
-

SpeckDL Language

-

A constraint-based specification language that defines what a system does, not how. Specs are small, stable, and machine-verifiable — the audit surface for regulated systems.

+

What Speckl Does

+

Speckl is a compiler for state machine specifications. You write what your system should do in SpeckDL — a typed specification language with states, actions, invariants, and guard conditions. The compiler produces five auditable artifacts from a single spec:

+ +
+
+
📜
+

PROV-O

+

W3C audit trail — who said what, when

-
-

Dark Provenance

-

A methodology where every behavior traces back to its source — a regulation, a design decision, a conversation. The provenance graph is always present, materialized on demand for audits or debugging.

+
+
📦
+

CycloneDX

+

Software Bill of Materials

-
-

Compiler

-

Compiles SpeckDL directly to Wasm through a deterministic pipeline — Z3 constraint solving, then code generation. No LLMs, no non-determinism. Same input, same output, every time.

+
+
📋
+

SPDX

+

License & compliance metadata

-
-

Reference Tools

-

Minimal implementations for SpeckDL parsing, Z3 verification, and provenance graph generation. The building blocks for tooling, not a production system.

+
+
⚡
+

TypeScript

+

Runnable state machine class

-
-

Ecosystem-First

-

The standard is the foundation. Consulting, SaaS tooling, and compliance APIs will build on it — validated through real-world use before they ship.

+
+
🔧
+

WASM

+

Verified WebAssembly binary

+ +

Fulfills NIST SA-11 (human-in-the-loop for automated outputs) — every AI-generated or hand-written spec is compiled through a deterministic pipeline. No LLMs in the compiler. Same input, same output, every time.

+ +
    +
  • Provenance is embedded by construction — not bolted on after the fact
    • +
  • 41 tests passing, < 2 seconds to run the full suite
    • +
  • 11 example specks: ToggleSwitch → TwoPhaseCommit → Paxos → Raft
    • +
  • Dual-target: TypeScript state machine classes + verified WASM from the same spec
    • +
  • Zero external services — everything runs locally
    • +
-

SpeckDL: A Specification Language

-

SpeckDL defines what a system does, not how. The compiler produces deterministic output: Z3 → Decision Structure → WASM. Same input, same output — every time. Every spec includes provenance: traceability to regulations, design decisions, and source conversations — embedded in the spec, not added later.

+

SpeckDL by Example

+

SpeckDL is a typed specification language for state machines. Define your states, actions, preconditions, and mutations — the compiler handles the rest.

- 
speck RetryHandler {
-  input: { operation: Operation, maxRetries: Nat }
-  output: Result
-  // Constraints the compiler proves via Z3
-  constraint: maxRetries <= 5
-  constraint: backoff(delay(n)) == delay(n-1) * 2
-  constraint: totalDelay < 30s
-  // Always-verified properties
-  verify: always(implies(attempt > 1, delay > 0))
-  // Dark provenance: where did this intent come from?
-  provenance: { regulation: "DO-178C 6.4.2.2" }
-  provenance: { design_decision: "ADR-0042" }
-  source: conversation ref "slack://C123/456"
-  review: manual
+  
// A simple toggle switch — compiles to TypeScript + WASM + 3 provenance artifacts
+spec ToggleSwitch {
+  type Status = enum { On, Off }
+
+  state {
+    status: Status = Status.Off
+  }
+
+  init Start() {
+    set status = Status.On
+  }
+
+  action Flip() {
+    require status == Status.On
+    set status = Status.Off
+    emit "TurnedOff"
+  }
+
+  action FlipBack() {
+    require status == Status.Off
+    set status = Status.On
+    emit "TurnedOn"
+  }
+
+  invariant "At most one pending action" {
+    !(status == Status.Flip && !(status == Status.FlipBack))
+  }
 }

+
+  

+    Type system: Int · Float · Bool · String · Enum · Struct · List<T> · Set<T> · Map<K,V>  | 
+    Keywords: spec · type · state · init · action · require · set · emit · invariant
+
-
-

Why Specifications?

- -
-
-

Small and Stable

-

Specs are orders of magnitude smaller than the code they generate. They change less often. The audit surface stays tractable.

+
+

Real Examples

+ +
+
+

Two-Phase Commit

+
45 lines · 5 actions
+

Classic distributed transaction coordinator. Voting phase, commit phase, abort path — fully specified with guard conditions.

-
-

Review the Boundary

-

If Speck→WASM compilation preserves semantics, human review at the spec boundary satisfies assurance requirements.

+
+

Paxos

+
120 lines · 3 safety invariants
+

Consensus for unreliable networks. Prepare, promise, accept, commit — with "only one value chosen" invariant.

-
-

Two-Species Collaboration

-

SpeckDL is the shared space humans and AI both work in — human-judgeable, AI-writable, and compiler-enforced to the binary.

+
+

Raft

+
230 lines · 8 actions · 3 invariants
+

Leader election, log replication, safety. The largest SpeckDL spec — demonstrates composition at scale.

+
+
+

Forgejo Issue Workflow

+
9 actions · 8 guard conditions
+

Real-world state machine: create → assign → review → merge → close. 5 temporal verification conditions.

+
+
+

Access Control

+
RBAC system · clean TS output
+

Role-based access with role addition, removal, and permission checks. One of 5 examples with zero TypeScript errors.

+
+
+

+ 6 more

+
DrugDosageCalculator · PaymentService · RetryHandler · TemperatureMonitor · AccountLedger · TigerBeetle
+

Browse all 11 examples →

-
-

Roadmap

- -
-
-

Phase A — Now

-

Open Standard: SpeckDL language, Dark Provenance methodology, reference implementations.

+
+

Strategy Ladder

+

Speckl follows a four-step strategy — each step validates the market before building the next:

+ +
+
+
Plan A
+
Open Standard
+
✅ Complete
+

MIT license. SpeckDL language + compiler + whitepaper — all public.

-
-

Phase B — Parallel

-

Consulting: Hands-on engagements with regulated-industry teams.

+
+
Plan B
+
Consulting
+
🔄 Drafted
+

Help regulated teams adopt spec-first workflows. One-pager ready.

-
-

Phase C — 3-9mo

-

SaaS: Spec editor, live Z3 verification, provenance graph browser.

+
+
Plan C
+
Developer Tool / SaaS
+
🔮 Future
+

Self-serve spec validation, CI/CD integration, team collaboration.

-
-

Phase D — 9-18mo

-

Compliance API: Audit reports, traceability matrices.

+
+
Plan D
+
Compliance API
+
🔮 Future
+

Automated audit reports, traceability matrices, regulatory filings.

+
+

Try It

+ + 
# Clone the repo
+git clone https://os.scoble.me/forgejo/sscoble/speckl.git
+cd speckl/compiler
+
+# Build and run tests (41 tests, ~2s)
+npm install
+npm test
+
+# Compile a spec to all 5 artifacts
+node dist/index.js ../examples/TwoPhaseCommit.speck -o out/twophase
+
+# Check TypeScript validity
+npx tsc --noEmit -p out/twophase
+
+# Validate WASM (requires wabt)
+wat2wasm out/twophase/TwoPhaseCommit.wat
+
+