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 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
Software Bill of Materials
License & compliance metadata
Runnable state machine class
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 is a typed specification language for state machines. Define your states, actions, preconditions, and mutations — the compiler handles the rest.
// 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
Classic distributed transaction coordinator. Voting phase, commit phase, abort path — fully specified with guard conditions.
Consensus for unreliable networks. Prepare, promise, accept, commit — with "only one value chosen" invariant.
Leader election, log replication, safety. The largest SpeckDL spec — demonstrates composition at scale.
Real-world state machine: create → assign → review → merge → close. 5 temporal verification conditions.
Role-based access with role addition, removal, and permission checks. One of 5 examples with zero TypeScript errors.
Speckl follows a four-step strategy — each step validates the market before building the next:
MIT license. SpeckDL language + compiler + whitepaper — all public.
Help regulated teams adopt spec-first workflows. One-pager ready.
Self-serve spec validation, CI/CD integration, team collaboration.
Automated audit reports, traceability matrices, regulatory filings.
# 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