docs: modernize README — state machine compiler, TLA+ examples, whitepaper v2 links
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
Drop outdated 'dark provenance' framing. Add current capabilities: - Working state machine compiler (WASM + TypeScript dual-target) - 5 artifact generation (WASM, TS, PROV-O, CycloneDX, SPDX) - TLA+ trilogy validation (TwoPhaseCommit, Paxos, Raft) - Complete whitepaper v2 (8 sections, ~19K words) - Speckl by Example tutorial - Distribution strategy - Strategy ladder with completion status Remove old roadmap table. Add known issues section linking engineering#9.
This commit is contained in:
Scott Scoble
parent
44a8406855
commit
65546fa6ba
1 changed files with 93 additions and 67 deletions
160
README.md
160
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.
|
||||
|
||||
|
||||
### 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
|
||||
|
||||
|
||||
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
|
||||
MIT © Scott Scoble / Greybeard Holdings, LLC
|
||||
|
||||
## Mirrors
|
||||
|
||||
- **Primary:** https://os.scoble.me/forgejo/sscoble/speckl
|
||||
- **Mirror:** https://codeberg.org/sscoble/speckl
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue