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. +
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.
- -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.
+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:
+ +W3C audit trail — who said what, when
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.
+Software Bill of Materials
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.
+License & compliance metadata
Minimal implementations for SpeckDL parsing, Z3 verification, and provenance graph generation. The building blocks for tooling, not a production system.
+Runnable state machine class
The standard is the foundation. Consulting, SaaS tooling, and compliance APIs will build on it — validated through real-world use before they ship.
+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.
+ +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 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
+ +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
+ +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
+ +Leader election, log replication, safety. The largest SpeckDL spec — demonstrates composition at scale.
+++Forgejo Issue Workflow
+ +Real-world state machine: create → assign → review → merge → close. 5 temporal verification conditions.
+++Access Control
+ +Role-based access with role addition, removal, and permission checks. One of 5 examples with zero TypeScript errors.
+++ 6 more
+ +- 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