diff --git a/README.md b/README.md index ac8d28d..72b9b80 100644 --- a/README.md +++ b/README.md @@ -1,105 +1,131 @@ # Speckl -**Spec-first development with dark provenance.** Write what your system should do. Prove it. Ship with full traceability. +**A judgement transport utility for AI-generated specifications.** Fulfills NIST SA-11 (human-in-the-loop for automated outputs). -Speckl is a multi-agent software development system where the primary artifact is the *specification*, not the code. Every behavior traces back to its source of intent — automatically. +Speckl is a specification language (SpeckDL) with a compiler that produces runnable software — WebAssembly, TypeScript, and provenance artifacts (PROV-O, CycloneDX, SPDX) — from a single source of truth. Write what your system should do. Prove it. Ship it. -## The Chain of Custody for Intent +## The Core Insight -Agents generate code. Humans own specifications. The chain of custody for intent stays intact. +AI generates code at machine speed. Humans own specifications. **SpeckDL is the shared space where both can work.** -That's the old framing. Here's the better one: +- **Human-judgeable** — SpeckDL is declarative enough that a person can inspect a spec and say "yes, this captures my intent." The compiled output is opaque; the spec is not. +- **AI-writable** — SpeckDL's constrained grammar and declarative semantics are tractable for LLMs to produce and reason about. Agents draft. Humans review. Both operate on the same semantic layer. +- **Compiled, not generated** — The SpeckDL compiler is deterministic. No LLMs in the compilation path. Same spec, same output — always. -**SpeckDL is the shared space that both humans and AI can work in.** +## What Speckl Does Now -- **Human-judgeable** — SpeckDL is declarative enough that a person can inspect a spec and say "yes, this captures my intent." The compiled Wasm is opaque; the spec is not. That's the audit trail. Intent is encoded in the spec *because* it is verifiable by a person. -- **AI-writable** — SpeckDL's constrained grammar and declarative semantics make it tractable for LLMs to produce and reason about. Agents can draft, iterate, and refactor specs at machine speed — in the same language the human reviews. - -The two properties together are symmetric: humans and agents collaborate in the same medium. The human provides direction and judgment. The agent provides speed and iteration. Both operate on the same semantic layer. - -SpeckDL compiles directly to **Wasm** through a deterministic pipeline. The compiler isn't just a code generator — it's the enforcement point that guarantees what the human signed off on is what gets executed. If it compiles to valid Wasm, the binary is faithful to the spec by construction. - -## Dark Provenance - -Every function, every branch, every side effect in your system is linked to the specification that motivated it. The provenance graph accumulates behind the scenes — invisible until you need it, but always complete. When an auditor asks "why does this code exist?", you don't search Jira. You query the graph. - -This isn't traditional traceability (forward-chaining from documents to code). It's the reverse: every runtime behavior backward-traces to its source specification. Specifications are small and stable. Code is derived. The audit surface stays tractable no matter how much code the system contains. - -## SpeckDL - -SpeckDL is the specification language at the core of Speckl. It defines *what* a system does, not *how*: +Speckl is a **working compiler** that turns formal specifications into multiple target representations: ``` -speck RetryHandler { - input: { operation: Operation, maxRetries: Nat } - output: Result - constraint: maxRetries <= 5 - constraint: backoff(delay(n)) == delay(n-1) * 2 - constraint: totalDelay < 30s - verify: always(implies(attempt > 1, delay > 0)) +.speckdl spec ──→ Wasm (WebAssembly) ← runnable, verified state machines + ├── TypeScript ← typed, importable classes + ├── PROV-O (RDF) ← W3C provenance standard + ├── CycloneDX SBOM ← OWASP software bill of materials + └── SPDX SBOM ← Linux Foundation SBOM standard +``` + +### State Machine Compilation (inspired by TLA+) + +```speckdl +spec ToggleSwitch { + state: Status = Off + enum Status = On | Off + + init: { + Status = Off + } + + action FlipSwitch { + require: true + if Status == On { + Status = Off + } else { + Status = On + } + } } ``` -SpeckDL compiles through a deterministic pipeline directly to Wasm: +This compiles to a runnable WebAssembly module with verified state transitions + guards, and to a type-safe TypeScript class. Both from the same spec. -![SpeckDL compilation pipeline](docs/diagrams/speckdl-pipeline.svg) +### Provenance Embedded at Compile Time -No LLMs in the compilation path. No non-determinism. Same input, same output — every time. +Every compilation embeds a complete provenance record — PROV-O RDF traces the spec → code derivation, CycloneDX and SPDX SBOMs capture the software supply chain. When an auditor asks "where did this behavior come from?", you query the graph, not Jira. -## Architecture +## Real-World Examples -![Architecture diagram](docs/diagrams/architecture.svg) +The compiler has been validated against: -- **Orchestrator** — client entry point, task decomposition -- **Team Leads** — manage specialized agents, elastic scaling -- **SMEs** — hyper-specialized single-task agents (verify, generate, document) -- **TillDone** — tasks complete when provable conditions are met, not when someone moves a card - -Teams self-replicate under load. The harness scales dynamically without human intervention. +| Example | Source | Status | +|---------|--------|--------| +| **ToggleSwitch** | SpeckDL tutorial | ✅ All 5 artifacts | +| **AccountLedger** | Banking ledger with debit/credit | ✅ All 5 artifacts | +| **TwoPhaseCommit** | TLA+ port | ✅ All 5 artifacts | +| **Paxos** | TLA+ port | ✅ All 5 artifacts | +| **Raft** | TLA+ port | ✅ All 5 artifacts | +| **TigerBeetleLedger** | Naive TigerBeetle core | ✅ All 5 artifacts (3 TS type errors in progress) | ## Getting Started -1. **Read the whitepaper:** [docs/whitepapers/dark-provenance.md](docs/whitepapers/dark-provenance.md) — the core methodology -2. **Read the strategy:** [docs/strategy.md](docs/strategy.md) — how Speckl grows from standard → consulting → SaaS → compliance -3. **Explore the SpeckDL spec:** [speckdl/SPEC.md](speckdl/SPEC.md) — language definition and examples -4. **Run the reference agent:** [reference-agent/](reference-agent/) — working tiered agent implementation - ```bash -# Clone the repo git clone https://os.scoble.me/forgejo/sscoble/speckl -cd speckl - -# Run the reference agent -cd reference-agent +cd speckl/compiler npm install -npm run dev + +# Compile an example to all 5 targets +node dist/index.js ../examples/ToggleSwitch.speck -o out/switch +ls out/switch/ +# ToggleSwitch.wat ToggleSwitch.ts ToggleSwitch.prov-o.jsonld +# ToggleSwitch.cyclonedx.json ToggleSwitch.spdx.json ``` -## Roadmap +### Key Documents -Speckl follows a phased strategy — the open standard fuels everything else: +- **[Whitepaper v2](docs/whitepaper-v2.md)** — Complete: 8 sections, ~19,000 words. Covers the spec-code gap, SpeckDL language, compiler architecture, embedded provenance, consensus protocols, compliance applications, related work, and roadmap. +- **[Speckl by Example](docs/speckl-by-example.md)** — Guided tutorial from ToggleSwitch through Raft, with TLA+ comparison table. +- **[Distribution Strategy](docs/distribution-strategy.md)** — Prioritized roadmap: Show HN → arXiv → blog → consulting pipeline. Conference landscape for 2026-2027. +- **[Strategy Ladder](docs/strategy.md)** — Open standard → Consulting → Developer Tool/SaaS → Compliance API. +- **[SpeckDL Spec](speckdl/SPEC.md)** — Language definition v0.2. +- **[State Machine Extension](speckdl/STATE-MACHINE-SPEC.md)** — `state`/`init`/`action` keywords, Set/Map/List types. -| Phase | Focus | Timeline | -|-------|-------|----------| -| **A — Open Standard** | SpeckDL language, Dark Provenance methodology, reference implementations | Now → 3mo | -| **B — Consulting** | Hands-on engagements with regulated-industry teams, validating the methodology | Now → 3mo (funds A) | -| **C — Developer Tool (SaaS)** | Self-serve platform: spec editor, live Z3 verification, provenance graph browser | 3 → 9mo | -| **D — Compliance API** | Enterprise provenance engine: audit reports, traceability matrices, compliance packs | 9 → 18mo | +## Strategy Ladder -The standard comes first. Adoption creates the market. The products follow. +| Phase | Focus | Status | +|-------|-------|--------| +| **A — Open Standard** | SpeckDL language, compiler, whitepaper, examples | ✅ **Complete** (compiler working, whitepaper done) | +| **B — Consulting** | Hands-on engagements with regulated-industry teams | 📋 One-pager drafted, awaiting review | +| **C — Developer Tool/SaaS** | Self-serve spec validation, provenance browser | 🔮 Future | +| **D — Compliance API** | Enterprise audit reports, traceability matrices | 🔮 Future | + +## Validation Status + +- **Compiler:** 41/41 tests passing (WASM + TypeScript codegen) +- **WASM E2E:** wabt assemble + instantiate + run verified +- **TypeScript:** Dual-target compilation — same spec produces both WASM and TS +- **TLA+ Trilogy:** TwoPhaseCommit, Paxos, Raft all compile (WAT validates through wabt) +- **Compiler Self-Spec:** `speckl-compile.speckdl` defines the Speckl compiler in SpeckDL — generates all 5 artifacts (known TypeScript errors tracked in engineering#9) + +## Known Issues + +The `rewriteExpr` function in the TypeScript generator applies spurious `this.state.` prefixes to function parameters in guard expressions. Tracked in [marcus/engineering#9](https://os.scoble.me/forgejo/marcus/engineering/issues/9). Parser also drops `precondition:`/`postcondition:` blocks on some action bodies. ## Contributing -Speckl is open source under the [MIT license](LICENSE). We welcome contributions: +Speckl is open source under the [MIT license](LICENSE). Contributions welcome: - **Language design** — refine SpeckDL syntax and semantics -- **Formal methods** — help verify the compilation pipeline -- **Compliance expertise** — validate the DO-178C, IEC 62304, ISO 26262 models -- **Agent development** — build and test the tiered agent harness -- **Documentation** — make dark provenance accessible to working developers +- **Compiler development** — TypeScript/Node.js, help fix open issues +- **Formal methods** — verify the compilation pipeline, add TLA+ examples +- **Compliance expertise** — validate regulatory models (NIST, IEC 62304, DO-178C) +- **Documentation** — tutorials, guides, case studies -Open an issue or submit a pull request. See [speckdl/SPEC.md](speckdl/SPEC.md) for the language spec and [docs/](docs/) for strategy and methodology documents. +Open an issue or submit a pull request. ## License -MIT © Scott Scoble / Greybeard Holdings, LLC \ No newline at end of file +MIT © Scott Scoble / Greybeard Holdings, LLC + +## Mirrors + +- **Primary:** https://os.scoble.me/forgejo/sscoble/speckl +- **Mirror:** https://codeberg.org/sscoble/speckl