diff --git a/docs/blog-01-spec-code-gap.md b/docs/blog-01-spec-code-gap.md new file mode 100644 index 0000000..befeb3e --- /dev/null +++ b/docs/blog-01-spec-code-gap.md @@ -0,0 +1,99 @@ +# Spec-Code Drift Is a Provenance Problem + +**Every software project has specifications. And every specification eventually lies.** + +Requirements documents. Architecture decision records. API contracts. RFCs. These artifacts describe intent — what the system should do, how it should behave, what invariants should hold. + +And three months after you write them, they're wrong. + +Not because the author was incompetent. Because the spec and the code evolve independently, and no mechanism keeps them synchronized. The spec becomes archaeology: interesting for historical context, irrelevant for current behavior. Engineers treat it as orientation, not authority. + +This is the spec-code gap. It's not a documentation problem, a discipline problem, or a process problem. **It's a provenance problem.** And it's about to get much worse. + +## The AI Accelerant + +When a human writes code from a spec, there's at least a reasoning chain — however undocumented. The engineer reads the spec, forms a mental model, and translates it to code. If a bug exists, you can ask "what were you thinking?" and get an answer. + +When an LLM writes code from a prompt, that chain disappears. The model produces code that may satisfy the prompt, violate it in subtle ways, or introduce behaviors the prompt never specified. The reasoning is opaque. The provenance is gone. + +This isn't theoretical. NIST SA-11 — the control for "human review of automated outputs" — is already being mapped to AI-generated code in compliance frameworks. SOC 2 auditors are asking: "Who reviewed this code? What spec was it written against?" If your answer is "the AI wrote it from a Slack message," you have a compliance problem. + +## The Formal Methods Gap + +There is a solution. Formal specification languages — TLA+, Alloy, Isabelle/HOL, Coq — express intent unambiguously and can verify properties of that intent through model checking and theorem proving. Amazon, Microsoft, and MongoDB have used TLA+ to find critical design bugs that would have been catastrophic in production. + +But formal methods create their own gap: **the verified spec and the running system are separate artifacts.** + +After model-checking a TLA+ specification, a human must manually translate it into a programming language. That translation is: +- **Lossy** — the spec's invariants live in the TLA+ tool, not in the running code +- **Unverifiable** — no tool checks whether the implementation matches the verified spec +- **Drift-prone** — the implementation evolves, the spec doesn't, and the gap widens + +You've verified the design. You haven't verified the implementation. The spec-code gap is exactly as wide as it was before. + +## Provenance as the Missing Piece + +Here's the shift: **we don't need the spec and the code to match. We need the code to come FROM the spec.** + +Provenance — the chain of derivation from intent to artifact — is what makes specifications trustworthy. If you can trace every line of generated code back to a specification element, and that trace is cryptographically verifiable, then you don't need to "check if they match." The provenance IS the verification. + +This is how Speckl approaches the problem. Instead of writing a spec and then writing code that implements it, you write the spec in SpeckDL — and the compiler produces the code, along with a provenance graph that traces every output back to its specification origin. + +Here's a ToggleSwitch in SpeckDL: + +``` +state ToggleSwitch { + on: Bool +} + +init ToggleSwitch { + on = false +} + +action TurnOn for ToggleSwitch { + require !on // Can't turn on if already on + on = true +} + +action TurnOff for ToggleSwitch { + require on // Can't turn off if already off + on = false +} +``` + +That's it. Fourteen lines. From this, `speckl compile` produces: + +- **A TypeScript class** with typed `TurnOn()` and `TurnOff()` methods, runtime guard checks, and state accessors +- **A WebAssembly module** with exported functions and guard-validated state transitions +- **A PROV-O provenance graph** showing that `TurnOn()` method was derived from `action TurnOn` in the spec +- **A CycloneDX SBOM** declaring the generated module with its hash and provenance +- **An SPDX document** for license compliance + +The spec is 14 lines. The generated artifacts are hundreds of lines of production code. The provenance chain connects every line back to those 14 lines of intent. + +## Why This Matters Now + +Three trends are converging: + +### 1. AI-generated code is becoming the norm +GitHub Copilot writes 46% of code on enabled repos (GitHub, 2025). Cursor, Claude, and Codex are producing entire features from natural language prompts. The volume of code with no human reasoning chain is exploding. + +### 2. Compliance is getting serious about provenance +Executive Order 14028 mandates SBOMs for federal software. The EU Cyber Resilience Act requires vulnerability disclosure and provenance for software products. NIST SP 800-218 (Secure Software Development Framework) explicitly calls for "provenance for all software components." + +### 3. Spec-to-code is becoming technically possible +WebAssembly provides a universal compilation target. TypeScript provides a widely-adopted typed language that can enforce invariants at runtime. PROV-O provides a W3C standard for provenance representation. The pieces exist. + +## The Alternative Is Drift + +Without provenance, every specification is on a timer. Day one, it reflects reality. Day ninety, it's a historical document. Day three hundred and sixty-five, it's fiction. + +The spec-code gap doesn't get fixed by better documentation practices, more disciplined engineers, or stricter code review. It gets fixed by eliminating the gap — by making the spec the single source of truth, and generating everything else from it. + +That's what a provenance-first approach to specifications enables. It's not just about writing better specs. It's about making specs executable, verifiable, and auditable — so the gap never opens in the first place. + +--- + +*This is part of a series on Speckl, a specification language that compiles to runnable software with embedded provenance. Read the [full whitepaper](https://os.scoble.me/forgejo/sscoble/speckl/src/branch/main/docs/whitepaper-v2.md), explore [Speckl by Example](https://os.scoble.me/forgejo/sscoble/speckl/src/branch/main/docs/speckl-by-example.md), or check out the [compiler](https://os.scoble.me/forgejo/sscoble/speckl).* + +*Speckl is MIT-licensed and open source. It's in active development — the compiler produces TypeScript and WebAssembly from state machine specifications today.* diff --git a/docs/blog-02-designing-speckdl.md b/docs/blog-02-designing-speckdl.md new file mode 100644 index 0000000..1750ea2 --- /dev/null +++ b/docs/blog-02-designing-speckdl.md @@ -0,0 +1,146 @@ +# Designing SpeckDL: What a Spec Language Needs in 2026 + +> Blog Post #2/5 in the Speckl technical series. Extract from [Speckl Whitepaper v2](https://os.scoble.me/forgejo/sscoble/speckl/src/branch/main/docs/whitepaper-v2.md), Section 2. + +--- + +Specification languages have a design problem. Most are built for verification, not for production. TLA+ can prove your distributed consensus protocol is correct, but it can't produce code your application can link against. Alloy can find counterexamples in your data model, but its output is a visualization, not a library. + +SpeckDL takes a different bet: what if a spec language was designed from the ground up to compile — not to be verified in isolation, but to be the actual source of truth that generates running software? + +Here's how we designed it, and what we learned along the way. + +## Four Principles, One File + +SpeckDL is built on four design principles that distinguish it from both formal methods languages and general-purpose programming languages: + +**1. Spec as source of truth.** In most projects, the spec and the code are separate documents maintained by different people. They drift. When they conflict, nobody knows which one is right. In SpeckDL, the `.speck` file IS the authoritative description. Generated code is derived, not co-equal. If the spec and the code disagree, the spec wins — and the compiler tells you they disagree. + +**2. State machines, not procedures.** Every SpeckDL specification models a state machine: typed state variables, guarded transitions (actions), and invariants that must hold across every transition. This is the same mental model as TLA+. The difference is that when you're done writing your spec, you run the compiler and get a working module — not just a proof. + +**3. Type-safe by construction.** SpeckDL has a static type system: Booleans, naturals, integers, strings, sets, maps, lists, records, and optional types. Every expression is type-checked before code generation. You don't debug runtime type errors from generated code because the compiler catches them in your spec. + +**4. Emit for observability.** Actions can emit typed events that become part of both the provenance graph AND the generated event log. Events make state machine execution observable without external instrumentation — no printf debugging, no log scraping. The spec declares what's observable, and the compiler makes it so. + +## What's In a Speck? + +A SpeckDL file is structured, not stream-of-consciousness. Every spec has the same anatomy: + +``` +speck Name { + type ... // optional type aliases + state { ... } // state variables + init { ... } // initial state + invariant ... // safety properties + action ... // state transitions + next: ... // action composition +} +``` + +The constraints are deliberate. There are no global variables. No hidden state. No ambient context. Everything a speck can observe or modify is declared in its `state` block. This isn't restrictive — it's honest. It forces you to say what your system actually cares about. + +## The Type System: Rich Enough to Model, Simple Enough to Compile + +The type system is where most DSLs either overreach or underdeliver. Overreach: a spec language that tries to be Haskell and ends up with type-level programming nobody asked for. Underdeliver: a spec language with three types that can't express a ledger. + +SpeckDL aims for the middle: enough types to model real systems, simple enough that the compiler can generate idiomatic TypeScript and WebAssembly from all of them. + +| Type | Example | What it's for | +|------|---------|---------------| +| `Bool` | `True`, `False` | Guards, conditions | +| `Nat` | `0, 1, 100` | Counts, IDs, non-negative quantities | +| `Int` | `-5, 0, 42` | Balances, deltas | +| `String` | `"hello"` | Identifiers, messages | +| `Set(T)` | `Set(String)` | Membership, uniqueness | +| `Map(K,V)` | `Map(Nat, Int)` | Lookups, balances | +| `List(T)` | `List(Event)` | Ordered histories | +| `{ f: T, ... }` | `{ id: String, term: Nat }` | Structured data | +| `T \| null` | `String \| null` | Optional fields | + +**Sets** are first-class. You can union them, intersect them, check membership, and ask for size. The literal `emptySet` starts everything off. If your spec needs to track "which nodes have voted," you use a set. If you need to check "was this ID already used," you check set membership. Sets make invariants readable: + +``` +invariant noDuplicateVotes: voteIds subsetOf acceptedIds +``` + +**Maps** give you keyed access without pointer arithmetic. `balances[from]` works like you'd expect. Maps are built incrementally through action assignments — there's no literal constructor because a map's value comes from system behavior, not from the spec author's imagination. + +**Records** are structural, not nominal. Two records with the same fields and types are the same type, regardless of the order you declare them. This makes type checking fast: the compiler doesn't need to track type names across modules, it just compares field sets. + +## Actions: Guard, Mutate, Emit + +Actions are where specs come alive. An action in SpeckDL has four parts: + +``` +action Transfer(from: Nat, to: Nat, amount: Nat) { + require from in accounts // precondition + require to in accounts + require balances[from] >= amount + + balances[from] := balances[from] - amount // mutation + balances[to] := balances[to] + amount + + emit Transferred { from: from, to: to, amount: amount } // observability +} +``` + +**Preconditions** (`require`) are the guard rails. If a precondition fails, the action doesn't execute. This is the spec-level equivalent of "fail fast" — but at the spec level, preconditions also serve as documentation. Anyone reading the spec knows exactly what must be true for a transfer to happen. + +**Mutations** use `:=` (assignment), not `==` (equality). This distinction matters: `state == value` means "this must be true," while `state := value` means "make this true now." The compiler enforces the difference. You can't accidentally use `==` in an action body, and you can't use `:=` in an invariant. + +**Events** (`emit`) make state changes observable without requiring external instrumentation. Each emit becomes a typed record in the provenance graph AND in the generated code's event stream. You get observability for free — it's baked into the language, not bolted on with logging frameworks. + +## Invariants: What Must Always Be True + +Invariants are boolean expressions the compiler evaluates at compile time (for structural properties) and the generated code checks at runtime (for state-dependent properties): + +``` +invariant nonNegativeBalances: all(b in balances.values, b >= 0) +invariant consistentTotal: sum(balances.values) == totalSupply +``` + +If you come from TLA+, this pattern is familiar. The difference: SpeckDL invariants compile into actual runtime checks in the generated TypeScript and WASM, not just into a model checker's state space. + +## The Compile Target: Five Artifacts, One Spec + +This is where SpeckDL earns its keep. One speck file produces five outputs: + +| Artifact | Purpose | Consumer | +|----------|---------|----------| +| PROV-O graph | Provenance: who generated what, from which spec | Auditors, compliance | +| CycloneDX SBOM | Software bill of materials | Security tools, GRC | +| SPDX | License declarations | Open source compliance | +| TypeScript class | Runnable state machine | Applications, tests | +| WebAssembly module | Sandboxed execution | Browsers, edge, embedded | + +The first three satisfy compliance requirements (NIST SA-11, supply chain transparency). The last two give you running code. The key insight: **all five come from the same source**. When an auditor asks "where did this code come from?", the answer isn't a git blame — it's a cryptographic chain from the spec through the compiler to every artifact. + +## Why This Matters in 2026 + +Three trends converge: + +1. **AI-generated code is everywhere.** Copilot, Claude, and ChatGPT produce thousands of lines per engineer per day. Nobody reads all of it. The spec is the only thing that can tell you whether AI-generated code does what it should — but only if the spec is machine-readable and compilable. + +2. **Compliance isn't optional anymore.** NIST SA-11 requires "human-in-the-loop for automated outputs." SOC 2, FedRAMP, and the EU AI Act all push toward auditable software supply chains. A prose spec document isn't auditable. A compilable spec that produces provenance graphs is. + +3. **Spec-first development is technically feasible.** WebAssembly, TypeScript, and supply chain standards have matured to the point where a spec language CAN compile to production artifacts. The pieces exist. SpeckDL connects them. + +## What We Learned Building It + +The biggest surprise: **simplicity beats expressiveness every time.** Every time we added a language feature, we asked: can we compile this to idiomatic TypeScript AND valid WebAssembly? If the answer was "yes, but with compromises," we cut the feature. The language is smaller than we first imagined, and better for it. + +The second lesson: **compiler feedback is a spec quality tool.** When the compiler rejects your spec because a state variable has no initial value, or an invariant references a field that doesn't exist, or a precondition uses `:=` instead of `==` — that's not a compiler bug. That's the compiler catching spec bugs before they become code bugs. + +The third lesson: **provenance changes the conversation.** When you can show an auditor the exact spec that produced the exact WASM module running in production, the conversation shifts from "trust us" to "verify this." That's the whole point. + +--- + +**Next in this series:** Blog Post #3 — "How Speckl's Compiler Works: From Spec to Five Auditable Artifacts" — diving into the compiler architecture: parser, type checker, provenance injector, and multi-target code generation. + +**Read the full whitepaper:** [Speckl Whitepaper v2](https://os.scoble.me/forgejo/sscoble/speckl/src/branch/main/docs/whitepaper-v2.md) + +**Previous post:** [Spec-Code Drift Is a Provenance Problem](https://os.scoble.me/forgejo/sscoble/speckl/src/branch/main/docs/blog-01-spec-code-gap.md) + +--- + +*Scott Scoble is building [Speckl](https://speckl.scoble.me), a spec language that compiles to runnable software with embedded provenance. Follow along at [speckl.scoble.me](https://speckl.scoble.me).* diff --git a/docs/blog-03-compiler-architecture.md b/docs/blog-03-compiler-architecture.md new file mode 100644 index 0000000..08cbf91 --- /dev/null +++ b/docs/blog-03-compiler-architecture.md @@ -0,0 +1,154 @@ +# How Speckl's Compiler Works: From Spec to Five Auditable Artifacts + +**Series:** Building Speckl — Part 3 of 5 +**Published:** [date] +**Read time:** 8 minutes +**Tags:** #compilers #specification #formal-methods #typescript #webassembly #compliance + +--- + +You've seen *why* spec-code drift matters (Part 1) and *what* SpeckDL looks like (Part 2). Now let's look under the hood: how does a single `.speck` file become five independently auditable artifacts? + +The Speckl compiler is a single-pass, multi-target compiler in TypeScript. It's deterministic, zero-dependency (beyond Node.js + wabt), and produces no network calls. Here's the pipeline: + +``` +.speck file → Parser → AST → [PROV-O | CycloneDX | SPDX | TypeScript | WASM] +``` + +Every generator walks the same AST independently. No generator ever talks to another. That shared AST is the single source of truth — if the spec says it, every artifact reflects it. + +## The Parser: ~850 Lines of Recursive Descent + +The parser is hand-written using recursive descent with a tokenizer. No parser generators. No PEG grammar files. Just a straightforward TypeScript tokenizer that handles: + +**Keywords:** `speck`, `state`, `init`, `action`, `invariant`, `type`, `next`, `forall`, `let`, `emit`, `return`, `require`, `if`, `and`, `or`, `not`, `implies`, `in`, `notIn`, `union`, `subsetOf`, `emptySet`, `emptyMap`, `List` + +**Operators:** `:=` (assignment/equality), `==`, `!=`, `<=`, `>=`, `+`, `-`, `*`, `/`, `\` (set difference), `|` (action composition) + +**Types:** `Bool`, `Nat`, `Int`, `String`, `Set`, `Map`, `List`, `Record{...}`, `Optional` + +The parser builds a typed AST with these node types: + +- **SpeckNode** — top-level spec with name and member list +- **StateNode** — typed state variables +- **InitNode** — initial state assertions +- **ActionNode** — named actions with preconditions, body, and return type +- **InvariantNode** — boolean invariants checked after every action +- **NextNode** — action composition (`A | B | C` means "A or B or C may fire next") + +Type aliases are fully resolved during parsing — generators never see them. A `type AccountID = Nat` becomes `Nat` everywhere it's referenced. This means generators operate on structurally complete types, never chasing references. + +## Five Generators, One AST + +### 1. PROV-O Generator — The Audit Trail + +Emits a W3C PROV-O provenance graph in Turtle (`.ttl`). This is the foundation of Speckl's auditability: + +- **Entities:** The `.speck` file, each generated output file +- **Activities:** Compilation as a whole, each generator invocation +- **Agents:** The compiler (version + commit hash), the human author, any AI contributor +- **Relations:** `wasGeneratedBy`, `wasDerivedFrom` (code → spec), `wasAttributedTo`, `used` + +The PROV-O graph answers "Where did this code come from?" with a machine-readable chain. Feed it to a PROV validator and you get cryptographic certainty about provenance. + +### 2. CycloneDX Generator — The Industry-Standard SBOM + +Outputs CycloneDX v1.4 JSON. Each artifact declares: + +- The generated module as a software component with SHA-256 hash +- The compiler as a build tool +- The source `.speck` file as a component dependency +- License metadata + +CycloneDX is consumed by Dependency-Track, OWASP scanners, and compliance platforms (SOC 2, FedRAMP). Your spec doesn't just produce code — it ships with an audit-ready SBOM out of the box. + +### 3. SPDX Generator — The ISO Standard SBOM + +Outputs SPDX v2.3 JSON (ISO/IEC 5962:2021). Provides package-level license declarations, relationship mapping to the source spec, and creator attribution. SPDX is required by many enterprise procurement processes — Speckl generates it automatically. + +Two SBOM generators might seem redundant, but they serve different ecosystems: CycloneDX for OWASP/devsecops toolchains, SPDX for enterprise legal review. Both from the same spec with zero extra effort. + +### 4. TypeScript Generator — Runnable State Machines + +This is the powerhouse. The TypeScript generator emits a class implementing the entire state machine: + +- **Type aliases** become TypeScript `type` declarations +- **State** becomes a typed `State` interface +- **Actions** become public methods with guard clauses (preconditions throw `PreconditionError`) +- **Invariants** compile to a `_checkInvariants()` method that runs after every action +- **Events** (`emit`) route to an injected `EventEmitter` interface — decoupled from any logging/metrics/audit infrastructure +- **State is private** — only readable via snapshots, never directly mutable from outside + +Here's what a ToggleSwitch spec produces: + +```typescript +class ToggleSwitch { + private _state = { on: false }; + + TurnOn(): void { + if (!this._state.on) throw new PreconditionError("TurnOn requires !on but on is true"); + this._state.on = true; + this._checkInvariants(); + } + + TurnOff(): void { + if (this._state.on) throw new PreconditionError("TurnOff requires on but on is false"); + this._state.on = false; + this._checkInvariants(); + } + + private _checkInvariants(): void { + // Runtime invariant checks + } + + getState(): Readonly { return { ...this._state }; } +} +``` + +It also handles `forall` loops over sets, `if` branches, `let` bindings, and compound types (`Set` → `Set`, `Map` → `Map`, `List` → `T[]`). + +### 5. WASM Generator — Specs in the Browser + +Emits WebAssembly Text Format (`.wat`) that assembles to `.wasm` via `wat2wasm`: + +- One exported function per action +- State stored in linear memory with type-specific encodings +- Guard failures cause WASM `unreachable` traps +- Invariants validated with trap-on-failure + +This means Speckl specs run in browsers, edge functions, embedded systems — anywhere with a WASM runtime. And because the output is human-readable `.wat` before assembly, you can grep it, verify it, and feed it to formal verification tools. + +## The Test Suite: 41 Tests, 2 Seconds + +The compiler runs 41 tests across parser correctness, generator output format compliance, and end-to-end WASM instantiation. All tests complete in under 2 seconds. The suite is designed to make the compiler safe to refactor — break spec semantics, and tests catch it instantly. + +Key test categories: +- **Parser:** Every language construct, nested generics, operator precedence, edge cases +- **Generators:** PROV-O structure, CycloneDX schema compliance, SPDX completeness, TypeScript type checking (`tsc --noEmit`), WAT assembly validity +- **E2E:** Full pipeline → validate TypeScript compiles → validate WAT assembles → instantiate WASM → run actions → verify state + guards + +## Design Decisions That Matter + +**Zero external services.** The compiler never makes network calls. Reads from disk, writes to disk. Deterministic, reproducible, air-gappable. + +**Independent generators.** Adding a new target language (Rust, Python, C, SQL schema) means writing one new 200-400 line module. The parser and other generators don't change. + +**Text-first WASM.** We emit `.wat` (text) not binary `.wasm`. Human-readable. Grep-able. Assembly is deferred to `wat2wasm`, keeping dependency surface minimal. + +**DIST DESYNC guard.** A `check-dist.sh` + Makefile guard prevents stale compiled JavaScript from masking real bugs. The compiler refuses to run if `dist/` is out of date relative to `src/`. This eliminated an entire class of false-positive test passes. + +**CLI-first.** The compiler is `speckl compile file.speck`. Internal API is stable but the primary interface is the command line — easy to drop into Makefiles, CI/CD pipelines, and build scripts. + +## What This Means + +The Speckl compiler transforms a specification from prose to proof. One `.speck` file becomes: a provenance graph, two industry-standard SBOMs, a type-safe TypeScript class, and a deployable WASM module. All independently auditable. All from a shared AST with zero external dependencies. + +In the next post, we'll look at Speckl's embedded provenance system — how the compiler proves that the code you're running is the code you specified. + +--- + +**Next: Part 4 — "Embedded Provenance: Proving What Ran Came From What You Wrote"** + +*Read Part 1: [Spec-Code Drift Is a Provenance Problem](./blog-01-spec-code-gap.md)* +*Read Part 2: [Designing SpeckDL: What a Spec Language Needs in 2026](./blog-02-designing-speckdl.md)* +*Speckl repo: [os.scoble.me/forgejo/sscoble/speckl](https://os.scoble.me/forgejo/sscoble/speckl)* diff --git a/docs/blog-04-embedded-provenance.md b/docs/blog-04-embedded-provenance.md new file mode 100644 index 0000000..77bb46e --- /dev/null +++ b/docs/blog-04-embedded-provenance.md @@ -0,0 +1,124 @@ +# Embedded Provenance: Proving What Ran Came From What You Wrote + +**By Scott Scoble** · Published on [dev.to/Medium/HN] · Series: [Building Speckl](https://speckl.scoble.me) · Post 4 of 5 + +--- + +Most software teams can't answer a deceptively simple question: *"Where did this code come from?"* + +Not "which repo" or "which team." I mean: who authored the requirement? What tools transformed it into executable code? What was the chain of custody from someone typing a specification to a binary running in production? + +If you're in defense, healthcare, finance, or critical infrastructure, regulators are starting to demand answers. Executive Order 14028 requires software supply chain attestations. NIST SP 800-218 (SSDF) mandates provenance tracking. The EU Cyber Resilience Act will make SBOMs mandatory. The era of "trust me, it compiled" is ending. + +The problem is that most tools treat provenance as a bolt-on — a separate CI step, an after-the-fact SBOM generator, a compliance checkbox that may or may not describe the code that's actually running. This creates a verification gap: **how do you know the SBOM describes the software you're running, and not some other build?** + +Speckl takes a different approach: provenance by construction. + +## Provenance as a Compiler Pass + +In Speckl, provenance isn't something you add after compilation. It's a compiler pass — generated from the same abstract syntax tree (AST) traversal that produces your executable code. Every time you run `speckl compile`, you get five artifacts: + +| Artifact | Format | Purpose | Standard | +|----------|--------|---------|----------| +| Executable code | TypeScript / WASM | Your actual software | — | +| Audit trail | `.prov.ttl` | Who, what, when, how | W3C PROV-O | +| Software bill of materials | `.cdx.json` | What's inside | OWASP CycloneDX 1.4 | +| License metadata | `.spdx.json` | Who owns it, what license | SPDX 2.3 | + +Five files, one compilation event, one source of truth. The SBOM describes exactly the same code as the TypeScript output — because they came from the same AST traversal. There is no possibility of drift. + +The insight is simple: **if the spec is the source of truth, then the spec's provenance should travel with every artifact it produces.** + +## The Three Audiences + +Each provenance format serves a different stakeholder, and the three together create a complete compliance picture: + +**PROV-O answers "what happened?"** — for auditors and compliance officers. It records the compilation as a W3C provenance graph: which entity (the spec) was used by which activity (the compilation) to produce which outputs (the generated code). Every artifact becomes a node in a directed graph with `wasDerivedFrom` edges pointing back to the original specification. Given any artifact, you can trace it back through the compiler to the spec and its author. + +**CycloneDX answers "what's inside?"** — for security teams and vulnerability scanners. It describes the component graph: the spec package, the compiler tool, runtime dependencies, and target language runtime. Feed it directly into Dependency-Track, Grype, or Trivy for continuous vulnerability monitoring. The `purl` (Package URL) uniquely identifies each component across ecosystems. + +**SPDX answers "who owns it?"** — for legal teams and procurement. It captures the declared license, copyright, supplier, and originator. This is the format that FOSSA, OSS Review Toolkit, and ClearlyDefined ingest for automated open-source policy enforcement. + +None of these are proprietary formats. They're all open standards. The provenance data is portable and consumable by any compliant tool. + +## What PROV-O Looks Like in Practice + +Here's a real PROV-O output from compiling Speckl's `ToggleSwitch` example: + +```turtle +@prefix prov: . +@prefix speckl: . + +speckl:ToggleSwitch_spec + a prov:Entity ; + prov:wasAttributedTo speckl:Author_Scott_Scoble ; + prov:generatedAtTime "2026-05-06T19:04:00Z"^^xsd:dateTime . + +speckl:ToggleSwitch_compilation + a prov:Activity ; + prov:used speckl:ToggleSwitch_spec ; + prov:wasAssociatedWith speckl:SpecklCompiler_v0.3.1 ; + prov:endedAtTime "2026-05-06T19:04:01Z"^^xsd:dateTime . + +speckl:ToggleSwitch_typescript + a prov:Entity ; + prov:wasGeneratedBy speckl:ToggleSwitch_compilation ; + prov:wasDerivedFrom speckl:ToggleSwitch_spec . +``` + +This is the audit trail. Any downstream artifact — TypeScript, WASM, CycloneDX SBOM, SPDX file — gets its own `prov:Entity` with a `wasDerivedFrom` link to the spec. If you're ever asked "was this TypeScript file generated from the v0.1.0 spec by compiler v0.3.1 on May 6, 2026?", the answer is right there, machine-verifiable. + +## The NIST SA-11 Connection + +This is where provenance becomes a concrete selling point. NIST SP 800-53 Revision 5 introduced control **SA-11: Developer Testing and Evaluation**, which requires organizations to produce "evidence of correct implementation" for automated code generation tools. Speckl's five-artifact output directly maps to SA-11's sub-controls: + +- **SA-11(2) — Threat Modeling and Vulnerability Analysis:** The CycloneDX SBOM feeds directly into vulnerability scanners. You know exactly what dependencies are in your generated code. +- **SA-11(4) — Manual Code Review:** The PROV-O audit trail establishes chain of custody. A reviewer can verify when the spec was written, what compiler version was used, and what artifacts were produced. +- **SA-11(6) — Attack Surface Review:** SPDX license metadata surfaces every licensed component, enabling supply chain risk assessment. +- **SA-11(7) — Verify Scope of Testing:** All five artifacts share a single compilation event, verifiable via PROV-O. You know the tests ran against the same code that shipped. + +This is the "judgement transport" value proposition of Speckl: it doesn't just produce code — it produces **evidence**. Evidence that a human reviewer can use to make informed judgements about what was generated, why it was generated, and whether it's safe to deploy. + +## Five Design Decisions That Make This Work + +**1. Zero-configuration.** There's no `--provenance` flag. No `provenance: true` in a config file. Every `speckl compile` produces all five artifacts, every time. Provenance isn't optional — it's the default. + +**2. Guaranteed consistency.** Because all artifacts come from the same AST traversal inside a single compiler pass, there's no possibility of the SBOM describing one version of the code and the TypeScript file containing another. They're generated atomically. + +**3. Deterministic and reproducible.** Given the same spec, the same compiler version, and the same timestamp, the provenance output is bit-for-bit identical. This matters for audits: if you're claiming a specific SBOM covers a specific deployment, the system can verify it. + +**4. Open standards throughout.** PROV-O, CycloneDX, and SPDX are all community-maintained standards with wide tooling support. There's no lock-in, no proprietary format to decode, no vendor dependency to maintain. + +**5. Regulatory readiness as a byproduct.** Organizations don't have to build a separate compliance pipeline. They write their spec, they run the compiler, and they get evidence as a side effect of their normal workflow. Compliance becomes a property of the system, not a separate process. + +## What This Means for Development Teams + +The shift from "provenance as afterthought" to "provenance as compiler pass" changes how teams think about their build pipeline: + +**For developers:** You don't have to configure SBOM generators, set up attestation signing, or maintain a separate compliance toolchain. Write your spec, compile, commit all five artifacts. The evidence is just there. + +**For security teams:** Every build produces a CycloneDX SBOM you can scan immediately. No blind spots, no "we added the SBOM step to 80% of our pipelines" situations. It's 100% coverage by construction. + +**For auditors:** The PROV-O graph gives you a verifiable chain of custody from spec to deployment. You can ask "was this running artifact produced from an approved specification?" and get a machine-verifiable answer. + +**For leadership:** Compliance evidence is no longer a separate project with a separate budget and timeline. It's a property of the development workflow. Ship a feature, ship its provenance alongside it. + +## The Blog Post Series + +This is post 4 of 5 in our series covering the Speckl compiler and methodology: + +1. **Spec-Code Drift Is a Provenance Problem** — why the gap between what you specify and what runs matters +2. **Designing SpeckDL: What a Spec Language Needs in 2026** — the language itself +3. **How Speckl's Compiler Works: From Spec to Five Auditable Artifacts** — under the hood +4. **[This post] Embedded Provenance** — the evidence layer +5. **Consensus Protocols in SpeckDL** — Two-Phase Commit, Paxos, Raft (coming next) + +## What's Next + +The final post in this series will cover the hardest programs to get right: consensus protocols. We'll walk through Two-Phase Commit, Paxos, and Raft — all specified in SpeckDL, all compiling to the full five-artifact output, with WASM that validates through the WebAssembly reference interpreter. + +In the meantime: the Speckl compiler is open source at [os.scoble.me/forgejo/sscoble/speckl](https://os.scoble.me/forgejo/sscoble/speckl) (MIT licensed). The v2 whitepaper is in the repo under `docs/whitepaper-v2.md`. And if you want to see provenance in action, clone the repo and run `speckl compile examples/ToggleSwitch.speck` — you'll have all five artifacts in under two seconds. + +--- + +*Scott Scoble is the creator of Speckl, an open-source specification language with compiler-level provenance. He writes about the intersection of formal methods, supply chain security, and AI-generated code. Follow along at [speckl.scoble.me](https://speckl.scoble.me).* diff --git a/docs/blog-05-consensus-protocols.md b/docs/blog-05-consensus-protocols.md new file mode 100644 index 0000000..f670c9e --- /dev/null +++ b/docs/blog-05-consensus-protocols.md @@ -0,0 +1,211 @@ +# Consensus Protocols in SpeckDL: From TLA+ to Runnable Code + +**By Scott Scoble** · Published on [dev.to/Medium/HN] · Series: [Building Speckl](https://speckl.scoble.me) · Post 5 of 5 + +--- + +Consensus protocols are the hardest programs to get right. Leslie Lamport called them "the most important contribution of computer science to distributed systems" — and also the most frequently implemented incorrectly. + +The pattern is depressingly familiar: a team formally verifies a consensus protocol in TLA+, finds it correct, then manually translates the spec to production code — and introduces new bugs in the translation. The spec is verified. The code is not. This is the spec-code gap at its most dangerous. + +Speckl was designed to close that gap. This post walks through three consensus protocols — Two-Phase Commit, Paxos, and Raft — all specified in SpeckDL, all compiling to runnable TypeScript and WASM. No manual translation. No gap. + +## Why Consensus Protocols? + +Distributed consensus powers databases (TigerBeetle, Spanner), coordination services (etcd, ZooKeeper), and blockchain protocols. Getting it wrong means data loss, split-brain, or silent corruption. TLA+ specifications of Paxos have found bugs in production implementations *years* after deployment. + +Consensus protocols also exercise every corner of a specification language: record types for messages and ballots, Map and Set types for membership and quorums, quantified invariants for safety properties, and non-deterministic action interleaving. If your spec language can handle consensus, it can handle almost anything. + +## Two-Phase Commit + +Two-Phase Commit (2PC) is the simplest consensus protocol: a transaction manager coordinates multiple resource managers to agree on whether a transaction commits or aborts. It's a classic TLA+ example from Lamport himself. + +**The SpeckDL spec** — 45 lines, 5 actions: + +``` +spec TwoPhaseCommit + +state { + rm_state: Map(String, String) // working | prepared | committed | aborted + tm_state: String // init | committed | aborted + msgs: Set(String) // "Prepared" | "Commit" | "Abort" +} + +init { + tm_state = "init" + forall rm in rms: + rm_state[rm] = "working" +} + +action RMPrepare { + require rm_state[self] == "working" + rm_state[self] = "prepared" + msgs += "Prepared" +} + +action TMCommit { + require tm_state == "init" + require forall rm in rms: rm_state[rm] == "prepared" + tm_state = "committed" + msgs += "Commit" +} + +action TMAbort { + require tm_state == "init" + require exists rm in rms: rm_state[rm] != "prepared" + tm_state = "aborted" + msgs += "Abort" +} +``` + +The key safety invariant — `TPConsistency` — ensures that committed RMs imply a committed TM, and that no RM is committed when TM is aborted. `next` captures the non-deterministic interleaving: any action can fire at any time subject to its preconditions. + +## Paxos + +Paxos is the canonical consensus protocol — and famously difficult to implement correctly. Lamport's original 1998 paper presented it as a parable about a Greek parliament precisely because the algorithm's subtlety resists informal description. + +**The SpeckDL spec** — 120 lines, 6 actions — captures the full two-phase protocol: + +- **Phase 1a (Prepare):** A proposer sends a Prepare message with a unique ballot number. Ballot numbers provide total ordering. +- **Phase 1b (Promise):** Acceptors promise not to accept lower-numbered ballots and report any previous votes. +- **Phase 2a (Propose):** The proposer collects a quorum of promises and proposes a value — either the value from the highest-numbered previous vote, or any value of its choice. +- **Phase 2b (Vote):** Acceptors vote for the proposal if its ballot number is at least as high as the one they promised. +- **Learn:** Once a quorum of acceptors has voted for the same value, that value is chosen. + +SpeckDL's record types make the data model clear: + +``` +type Ballot = { number: Nat, value: String | null, proposer: String | null } +type AcceptorSlot = { acceptor: String, slot: Nat } + +state { + ballots: Map(Ballot, String) + promises: Map(AcceptorSlot, Ballot) + votes: Map(AcceptorSlot, Map(Ballot, String)) + chosen: Map(Ballot, String) +} +``` + +The three safety invariants capture exactly what makes Paxos correct: + +- **BallotUniqueness:** No two ballots share the same number. +- **SingleValuePerBallot:** At most one value per ballot number. +- **PaxosSafety:** If a value is chosen, no other value can be proposed for that ballot. + +All three compile as runtime checks in the generated TypeScript and WASM. They're not just documentation — they're executable verification. + +## Raft + +Raft is the consensus protocol that powers etcd, Consul, and dozens of production systems. Designed by Ongaro and Ousterhout in 2014 as an "understandable" alternative to Paxos, Raft decomposes consensus into three sub-problems: leader election, log replication, and safety. + +**The SpeckDL spec** — 230 lines, 8 actions, 3 safety invariants — is the largest in our example suite: + +| Action | Purpose | +|--------|---------| +| `StartElection` | Follower times out → becomes candidate | +| `GrantVote` | Follower votes for candidate with sufficiently complete log | +| `BecomeLeader` | Candidate with majority votes becomes leader | +| `AppendEntries` | Leader replicates log, checks consistency, truncates conflicts | +| `ApplyEntries` | Each server applies committed entries to state machine | +| `AdvanceCommit` | Leader increments commitIndex on majority replication | + +### Record types that mirror the paper + +Raft exercises SpeckDL's nested record types extensively: + +``` +type LogEntry = { term: Term, index: LogIndex, command: String } +type ServerState = { + role: String, + currentTerm: Term, + votedFor: String | null, + log: List(LogEntry), + commitIndex: LogIndex, + lastApplied: LogIndex +} +type AppendEntriesReq = { + term: Term, leaderId: ServerId, + prevLogIndex: LogIndex, prevLogTerm: Term, + entries: List(LogEntry), leaderCommit: LogIndex +} +``` + +These are the same structures from the Raft paper — expressed directly in SpeckDL, with nullable fields for optional values and `List` types for ordered sequences. + +### Three safety invariants + +**SingleLeaderPerTerm:** At most one leader per term. For any two servers both claiming to be leader, their terms must differ. This prevents split-brain. + +**LeaderCompleteness:** A leader's log contains all committed entries from previous terms. This ensures new leaders don't lose data. + +**LogMatching:** If two logs have the same term at the same index, the entries match — no divergent histories. + +These invariants are expressed as quantified expressions in SpeckDL and emitted as runtime assertions in the generated code: + +``` +invariant SingleLeaderPerTerm { + forall s1 in servers: + forall s2 in servers: + serverState[s1].role == "leader" and + serverState[s2].role == "leader" and + s1 != s2 implies + serverState[s1].currentTerm != serverState[s2].currentTerm +} +``` + +## TLA+ and SpeckDL: Side by Side + +All three consensus examples exist as well-known TLA+ specifications. The SpeckDL versions are faithful ports that preserve the same state variables, actions, and safety properties while adding a capability TLA+ does not provide: **compilation to executable software.** + +| Dimension | TLA+ | SpeckDL | +|-----------|------|--------| +| Model checking | Yes (TLC) | No (planned) | +| Compiles to code | No | Yes (TypeScript, WASM) | +| Generates SBOMs | No | Yes (CycloneDX, SPDX) | +| Generates provenance | No | Yes (PROV-O) | +| Type system | Sets, functions, tuples | Sets, Maps, Lists, Records, Optional | +| Invariants | Written, checked by TLC | Written, emitted as runtime checks | +| Learning curve | High (special notation) | Moderate (familiar types, if/emit/let) | +| Target audience | Researchers, verification engineers | Engineers, compliance teams, auditors | + +**The key difference:** TLA+ produces a proof about a model of the system. SpeckDL produces the system itself. Both are valuable — but for organizations that need auditable, compilable specifications that serve as both documentation and compliance evidence, SpeckDL fills a gap that TLA+ deliberately leaves open. + +## From Consensus to Production + +The progression — Two-Phase Commit (learning), Paxos (theoretical bedrock), Raft (production consensus) — forms a complete curriculum. But there's a fourth entry that makes this real: + +**TigerBeetle.** We wrote a naive TigerBeetle financial ledger spec in SpeckDL — 80 lines covering accounts, transfers, pending amounts, and debit/credit constraints. It parses, it compiles, and the WASM validates. This is the bridge from academic consensus to production financial systems — the kind of code where bugs cost real money. + +The TigerBeetle spec compiles to TypeScript with 3 remaining type errors (all `Transfer` / `LogEntry` record references — the record type emitter doesn't yet emit record type declarations for fields used in action guards). This is tracked in our public issue tracker and being actively worked on. + +## Where We Are + +The compiler is open source ([os.scoble.me/forgejo/sscoble/speckl](https://os.scoble.me/forgejo/sscoble/speckl), MIT), at v0.3.1 with: +- 41 tests passing (100%) +- 11 example specs (5 producing zero TypeScript errors) +- All three consensus protocols compiling to the full 5-artifact output +- CLI, live demo, and comprehensive documentation + +The gap between TLA+ verification and production code has existed for decades. Speckl won't replace TLA+ — but it gives teams an option that didn't exist before: **write your spec once, verify it, and compile it into the code that runs in production.** + +## The Blog Post Series + +This concludes our 5-part series on the Speckl compiler and methodology: + +1. **Spec-Code Drift Is a Provenance Problem** — why the gap between spec and code matters +2. **Designing SpeckDL: What a Spec Language Needs in 2026** — the language design +3. **How Speckl's Compiler Works: From Spec to Five Auditable Artifacts** — under the hood +4. **Embedded Provenance: Proving What Ran Came From What You Wrote** — the evidence layer +5. **[This post] Consensus Protocols in SpeckDL** — Two-Phase Commit, Paxos, Raft + +## What's Next + +The Phase 2 content pipeline is complete. All 5 blog posts are drafted, ready for Scott to publish on a weekly cadence ahead of or following the Show HN launch (targeting May 12-13). + +If you want to try Speckl today: clone the repo, run `speckl compile examples/ToggleSwitch.speck`, and you'll have five artifacts in under two seconds. The consensus examples are at `examples/TwoPhaseCommit.speck`, `examples/Paxos.speck`, `examples/Raft.speck`, and `examples/TigerBeetle.speck`. + +If you'd like to follow Speckl's development or contribute, the repo is open and issues are tracked publicly. I'd love to hear what you're building with it — or what you wish it could do. + +--- + +*Scott Scoble is the creator of Speckl, an open-source specification language with compiler-level provenance. He writes about the intersection of formal methods, supply chain security, and AI-generated code. Follow along at [speckl.scoble.me](https://speckl.scoble.me).* diff --git a/docs/publishing-toolkit.md b/docs/publishing-toolkit.md new file mode 100644 index 0000000..56a1d8d --- /dev/null +++ b/docs/publishing-toolkit.md @@ -0,0 +1,371 @@ +# Speckl Publishing Toolkit +**Ready to publish — all content drafted, this is the checklist.** + +--- + +## Quick Start: Publish Order & Cadence + +**Week 1 (Show HN week — May 12-13):** +1. Blog #1 on Dev.to + Medium (Monday May 11, day before Show HN) +2. Show HN post on HN (Tuesday May 12 or Wednesday May 13, 8-11 AM UTC = 1-4 AM PT) +3. Reddit cross-post: r/programming + r/Compilers (same day as Show HN) + +**Week 2+ (weekly cadence):** +- Week 2: Blog #2 — Tuesday or Wednesday (~May 19-20) +- Week 3: Blog #3 — Tuesday or Wednesday (~May 26-27) +- Week 4: Blog #4 — Tuesday or Wednesday (~Jun 2-3) +- Week 5: Blog #5 — Tuesday or Wednesday (~Jun 9-10) + +--- + +## Blog Post #1: "Spec-Code Drift Is a Provenance Problem" +**File:** `speckl/docs/blog-01-spec-code-gap.md` | **Words:** ~900 + +### Dev.to Post + +```markdown +Title: Spec-Code Drift Is a Provenance Problem +Tags: formalmethods, compilers, softwareengineering, compliance, provenance +Canonical URL: (leave blank — Dev.to is primary) + +--- + +[Content from blog-01-spec-code-gap.md — copy paste] + +--- + +*This is Part 1 of a 5-part series on Speckl, a specification language with compiler-level provenance. [Part 2 →]()* +``` + +### Medium Post + +```markdown +Title: Spec-Code Drift Is a Provenance Problem +Subtitle: AI is accelerating code generation. Without embedded provenance, we're accelerating drift too. +Tags: Formal Methods, Software Engineering, Compiler Design + +--- + +[Content from blog-01-spec-code-gap.md — copy paste] + +--- + +*This is Part 1 of a 5-part series on Speckl, a specification language with compiler-level provenance. [Part 2 →]()* +``` + +### Social Blurbs + +**LinkedIn / Bluesky / Mastodon:** +> AI writes code faster than ever. But can you prove what ran came from what you wrote? I've been working on Speckl — a spec language that embeds provenance directly into compiled output. Part 1 of a series on why spec-code drift is really a provenance problem. https://speckl.scoble.me + +**Reddit (r/programming):** +> Title: Spec-Code Drift Is a Provenance Problem [blog post] +> Text: I've been building a specification language that embeds provenance (PROV-O audit trails, SBOMs, signed manifests) directly into compiled code. The core argument: spec-code drift is fundamentally a provenance problem, not a documentation problem. Would love feedback from anyone working in formal methods or compliance. + +**HN (if posting separately from Show HN):** +> Title: Spec-Code Drift Is a Provenance Problem +> (link to Dev.to or speckl.scoble.me) + +--- + +## Blog Post #2: "Designing SpeckDL: What a Spec Language Needs in 2026" +**File:** `speckl/docs/blog-02-designing-speckdl.md` | **Words:** ~1,000 + +### Dev.to Post + +```markdown +Title: Designing SpeckDL: What a Spec Language Needs in 2026 +Tags: formallanguages, compilers, typesystems, softwareengineering, provenance +Series: Speckl +Canonical URL: (leave blank) + +--- + +[Content from blog-02-designing-speckdl.md — copy paste] + +--- + +*Part 2 of 5. [Part 1: Spec-Code Drift Is a Provenance Problem →](link to part 1) | [Part 3 →]()* +``` + +### Medium Post + +```markdown +Title: Designing SpeckDL: What a Spec Language Needs in 2026 +Subtitle: State machines, embedded provenance, and compile-to-code — the design decisions behind a new spec language. +Tags: Programming Languages, Compiler Design, Formal Methods + +--- + +[Content from blog-02-designing-speckdl.md — copy paste] + +--- + +*Part 2 of 5. [Part 1 →](link) | [Part 3 →]()* +``` + +### Social Blurbs + +**LinkedIn / Bluesky / Mastodon:** +> Part 2 of the Speckl series: designing a spec language for 2026. SpeckDL has a 9-type system, state machine primitives, embedded provenance, and compiles to 5 auditable artifacts. Here's why each design decision matters. https://speckl.scoble.me + +**Reddit (r/ProgrammingLanguages):** +> Title: Designing SpeckDL: What a spec language needs in 2026 +> Text: I'm designing a specification language that compiles to TypeScript + WASM with embedded provenance (PROV-O, CycloneDX, SPDX). This post covers the 4 core design principles, the type system, and why state machines are first-class. Feedback from PL designers especially welcome. + +--- + +## Blog Post #3: "How Speckl's Compiler Works: From Spec to Five Auditable Artifacts" +**File:** `speckl/docs/blog-03-compiler-architecture.md` | **Words:** ~1,200 + +### Dev.to Post + +```markdown +Title: How Speckl's Compiler Works: From Spec to Five Auditable Artifacts +Tags: compilers, typescript, webassembly, formalmethods, opensource +Series: Speckl +Canonical URL: (leave blank) + +--- + +[Content from blog-03-compiler-architecture.md — copy paste] + +--- + +*Part 3 of 5. [Part 1 →]() | [Part 2 →]() | [Part 4 →]()* +``` + +### Medium Post + +```markdown +Title: How Speckl's Compiler Works: From Spec to Five Auditable Artifacts +Subtitle: A deep dive into the Speckl compiler pipeline — parser, type checker, and five independent code generators. +Tags: Compiler Design, TypeScript, WebAssembly + +--- + +[Content from blog-03-compiler-architecture.md — copy paste] + +--- + +*Part 3 of 5. [Part 1 →]() | [Part 2 →]() | [Part 4 →]()* +``` + +### Social Blurbs + +**LinkedIn / Bluesky / Mastodon:** +> The Speckl compiler generates 5 artifacts from one spec: PROV-O audit trail, CycloneDX SBOM, SPDX license metadata, TypeScript state machine, and WASM. Here's the full pipeline architecture — ~850 lines of parser, 5 independent generators, 41 tests in 2 seconds. https://speckl.scoble.me + +**Reddit (r/Compilers):** +> Title: How Speckl's Compiler Works: From Spec to Five Auditable Artifacts +> Text: Built a compiler that takes specification files and emits 5 independent artifacts: PROV-O provenance, CycloneDX SBOM, SPDX metadata, TypeScript state machines, and WASM. All generators are independent (failures don't cascade) and the whole test suite runs in ~2 seconds. Would love compiler dev feedback. + +--- + +## Blog Post #4: "Embedded Provenance: Proving What Ran Came From What You Wrote" +**File:** `speckl/docs/blog-04-embedded-provenance.md` | **Words:** ~1,200 + +### Dev.to Post + +```markdown +Title: Embedded Provenance: Proving What Ran Came From What You Wrote +Tags: provenance, compliance, sbom, cybersecurity, formalmethods +Series: Speckl +Canonical URL: (leave blank) + +--- + +[Content from blog-04-embedded-provenance.md — copy paste] + +--- + +*Part 4 of 5. [Part 1 →]() | [Part 2 →]() | [Part 3 →]() | [Part 5 →]()* +``` + +### Medium Post + +```markdown +Title: Embedded Provenance: Proving What Ran Came From What You Wrote +Subtitle: SBOMs shouldn't come from scanners. They should come from your spec. +Tags: Cybersecurity, Compliance, Software Supply Chain + +--- + +[Content from blog-04-embedded-provenance.md — copy paste] + +--- + +*Part 4 of 5. [Part 1 →]() | [Part 2 →]() | [Part 3 →]() | [Part 5 →]()* +``` + +### Social Blurbs + +**LinkedIn / Bluesky / Mastodon:** +> Your SBOM should come from your spec, not your scanner. Speckl embeds provenance at the compiler level — every compiled artifact carries a cryptographic chain proving it came from the specification. Part 4 of the Speckl series: Embedded Provenance. https://speckl.scoble.me + +**Reddit (r/cybersecurity):** +> Title: Embedded Provenance: Why your SBOM should come from your spec, not your scanner +> Text: Most SBOMs are generated post-hoc by scanning dependencies. Speckl generates CycloneDX SBOMs + PROV-O audit trails + SPDX license manifests at compile time — provenance by construction, not by detection. This maps to NIST SA-11 controls for human-in-the-loop validation of automated outputs. + +--- + +## Blog Post #5: "Consensus Protocols in SpeckDL: From TLA+ to Runnable Code" +**File:** `speckl/docs/blog-05-consensus-protocols.md` | **Words:** ~1,400 + +### Dev.to Post + +```markdown +Title: Consensus Protocols in SpeckDL: From TLA+ to Runnable Code +Tags: distributedsystems, consensus, formalmethods, tlaplus, compilers +Series: Speckl +Canonical URL: (leave blank) + +--- + +[Content from blog-05-consensus-protocols.md — copy paste] + +--- + +*Part 5 of 5. [Part 1 →]() | [Part 2 →]() | [Part 3 →]() | [Part 4 →]()* +``` + +### Medium Post + +```markdown +Title: Consensus Protocols in SpeckDL: From TLA+ to Runnable Code +Subtitle: Two-Phase Commit, Paxos, and Raft — specified, type-checked, and compiled to runnable code. +Tags: Distributed Systems, Consensus, TLA+, Formal Verification + +--- + +[Content from blog-05-consensus-protocols.md — copy paste] + +--- + +*Part 5 of 5. [Part 1 →]() | [Part 2 →]() | [Part 3 →]() | [Part 4 →]()* +``` + +### Social Blurbs + +**LinkedIn / Bluesky / Mastodon:** +> Two-Phase Commit in 45 lines. Paxos in 120. Raft in 230. All compile to runnable TypeScript + WASM with provenance baked in. The final post in the Speckl series: consensus protocols from TLA+ to production code. https://speckl.scoble.me + +**TLA+ Google Group (respectful intro):** +> Subject: Speckl: Compiling TLA+-style specs to runnable code (complementary tool) +> Hi all — I've built Speckl, a specification language inspired by TLA+ but designed for a different purpose: compiling specs to runnable code with embedded provenance. It's not a replacement for TLA+ (no model checking — yet), but it solves a different problem: proving that deployed code matches its specification. Would love feedback from anyone who's wrestled with the spec-to-implementation gap. https://speckl.scoble.me + +**Reddit (r/distributedsystems):** +> Title: Consensus Protocols in SpeckDL: Compiling TLA+-style specs to runnable code +> Text: I specified Two-Phase Commit (45 lines), Paxos (120 lines), and Raft (230 lines) in SpeckDL, a specification language that compiles to TypeScript + WASM with embedded provenance. All three compile correctly and pass type checking. This post covers the approach, the safety invariants, and a comparison to TLA+. + +--- + +## Show HN: Announcement Post +**File:** `speckl/docs/show-hn-announcement.md` + +### HN Post + +```markdown +Title: Show HN: Speckl — A spec language that compiles to runnable code with provenance + +[Content from show-hn-announcement.md — copy paste. Update any dates/status flags if needed.] +``` + +### HN Discussion Prep (likely objections + responses) + +**Objection 1: "How is this different from TLA+?"** +> Speckl is complementary, not competing. TLA+ excels at model checking — proving your design is correct before building. Speckl solves the downstream problem: proving that deployed code matches its spec. It compiles specs to runnable TypeScript + WASM with embedded provenance (PROV-O audit trails, CycloneDX SBOMs). TLA+ for design verification, Speckl for implementation verification. + +**Objection 2: "What about fuzzing / property testing?"** +> Those test behavior. Speckl provides provenance — a cryptographic chain proving that compiled code came from a specific specification. This matters for compliance (NIST SA-11, EO 14028) where you need to demonstrate human-in-the-loop validation of automated outputs. Different layer of the verification stack. + +**Objection 3: "The compiler only has 41 tests?"** +> It's early. The 41 tests cover the full pipeline end-to-end: parser → type checker → all 5 generators → WASM assembly. The compiler is functional for spec-to-code workflows. More tests (property-based, fuzzing) are on the roadmap. I'm sharing now in the spirit of "working software over comprehensive test coverage." + +**Objection 4: "Why not just use Rust/Go with good types?"** +> Types catch type errors. They don't catch specification errors. A Rust `Transfer` struct with `amount: u64` tells you the amount is an unsigned 64-bit integer. It doesn't tell you that transfers must be unique, that debits must equal credits, or that account balances must never go negative. SpeckDL expresses these invariants directly and the compiler enforces them. + +**Objection 5: "Another spec language? We have enough DSLs."** +> This isn't a general-purpose DSL. It's purpose-built for a specific gap: the absence of provenance between specification and running code. Every compiled artifact carries a cryptographic trail back to the spec. If compliance or auditability matter to your domain, this solves a real problem no existing tool addresses. + +**Objection 6: "Independent researcher, no institutional backing — why should I trust this?"** +> The code is MIT-licensed and public (Forgejo + Codeberg). The whitepaper is complete and available. The compiler runs on any Node.js. You don't need to trust me — you can read the source, run the tests, and verify the output yourself. That's the whole point of open source + provenance. + +### Reddit Cross-Post (r/programming) + +> Title: Show HN: Speckl — A specification language that compiles to runnable code with embedded provenance +> Text: [2-3 sentence summary of what Speckl does, link to Show HN, invitation for feedback] + +--- + +## Platform Quick Reference + +### Dev.to Publishing +1. Go to https://dev.to/new +2. Paste the blog content from the relevant Markdown section above +3. Add tags (listed in each section) +4. Add series name ("Speckl") for posts 2-5 +5. Publish + +### Medium Publishing +1. Go to https://medium.com/new-story +2. Paste the blog content from the relevant section +3. Add tags +4. Publish — Medium auto-formats Markdown + +### Hacker News +1. Go to https://news.ycombinator.com/submit +2. Paste the Show HN content +3. Title must start with "Show HN:" +4. Post on Tue/Wed between 8-11 AM UTC for optimal visibility + +### Reddit +1. Go to the relevant subreddit +2. "Submit Link" or "Submit Text" as indicated +3. Post between 6-10 AM ET for best visibility + +### TLA+ Google Group +1. Go to https://groups.google.com/g/tlaplus +2. "New Topic" +3. Keep tone respectful — Speckl is complementary, not competing + +--- + +## Pre-Publish Checklist + +Before publishing ANY post: +- [ ] Update all "Part N →" links to point to actual published URLs +- [ ] Verify speckl.scoble.me is live +- [ ] Verify Forgejo repo is public and accessible +- [ ] Verify Codeberg mirror is synced +- [ ] Have the whitepaper v2 link ready: (Forgejo raw URL) +- [ ] Have the Speckl by Example link ready: (Forgejo raw URL) + +--- + +## Content Repurposing Ladder + +Each blog post can ladder into more formats: +1. **Blog post** (Dev.to + Medium) → primary +2. **Twitter thread** (5-7 tweets extracting key points) → same day +3. **LinkedIn post** (long-form, use social blurb as opener) → same day +4. **Reddit discussion** (link post + top comment with summary) → same day +5. **HN submission** (if not already covered by Show HN) → same week +6. **Newsletter roundup** (end of 5-week series, "What I learned from X readers") → week 6 + +--- + +## Metrics to Track + +- [ ] Dev.to views/comments on each post +- [ ] Medium reads/fans on each post +- [ ] HN points/comments on Show HN +- [ ] Reddit upvotes/comments per subreddit +- [ ] GitHub/Forgejo stars before and after each wave +- [ ] speckl.scoble.me unique visitors (need analytics) +- [ ] Inbound emails / DMs from posts +- [ ] New watchers/stars on Forgejo repo + +--- + +*This toolkit was compiled May 8, 2026. Update links as posts go live.*