From 940b959efb521791d20dde6cd150b1fc0eff72d4 Mon Sep 17 00:00:00 2001 From: Scott Scoble Date: Thu, 7 May 2026 00:18:59 -0700 Subject: [PATCH] Whitepaper v2 Section 7: Related Work (~2,500 words) Comprehensive comparison of SpeckDL against: - TLA+/PlusCal (model checking vs. runtime compilation) - Alloy (structural vs. behavioral modeling) - Coq/Rocq (static proofs vs. dynamic enforcement) - Dafny (verified code vs. spec-as-code) - Event-B, UML/SysML, P (Microsoft), OpenAPI/gRPC - SBOM tools: Syft/Grype, SLSA, in-toto Includes positioning table across 7 tools on 6 dimensions. Defines niche: specification language with compiler-level provenance, designed for teams that need evidence of correctness more than proof. --- docs/whitepaper-v2.md | 136 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 135 insertions(+), 1 deletion(-) diff --git a/docs/whitepaper-v2.md b/docs/whitepaper-v2.md index 331f405..5318594 100644 --- a/docs/whitepaper-v2.md +++ b/docs/whitepaper-v2.md @@ -1069,7 +1069,141 @@ The upfront cost: spec authoring. The recurring savings: all evidence production ## 7. Related Work -*[Section 7: Comparison with TLA+, Alloy, Coq, Dafny, and code generation approaches]* +Speckl and SpeckDL sit at the intersection of several well-established fields: formal specification languages, software verification tools, SBOM/provenance standards, and code generation frameworks. This section surveys the adjacent work and explains where Speckl fits — and where it deliberately chooses a different path. + +### 7.1 Formal Specification Languages + +#### TLA+ + +TLA+ (Temporal Logic of Actions), developed by Leslie Lamport, is the most direct ancestor of SpeckDL. Both languages express systems as state machines with actions, invariants, and typed variables. TLA+ has been used to specify and verify industrial systems including Amazon Web Services (S3, DynamoDB), Microsoft Azure, and MongoDB. + +**What SpeckDL borrows from TLA+:** +- State machine semantics with non-deterministic action interleaving (`next: A | B | C`) +- Invariants as safety properties checked at every state transition +- Record types for structured state +- Set, Map, and quantified expressions (`forall`) + +**What SpeckDL does differently:** +- **Compilation, not model checking.** TLA+ uses TLC (the TLA+ model checker) to exhaustively search state spaces for invariant violations. SpeckDL generates production code that enforces invariants at runtime. This means SpeckDL catches the same class of errors, but in production rather than a sandbox. +- **Provenance by default.** Every SpeckDL compilation produces PROV-O, CycloneDX, and SPDX artifacts. TLA+ produces none of these — its outputs are verification reports, not auditable evidence. +- **Type system with generics.** SpeckDL's `Set`, `Map`, `List` give compiler-enforced type safety. TLA+ is untyped; type errors manifest as model-checking failures. +- **Learning curve.** TLA+ requires learning temporal logic notation and PlusCal syntax. SpeckDL uses familiar programming keywords (`state`, `action`, `require`, `emit`, `let`) with conventional block structure. A developer who knows TypeScript or Python can read a SpeckDL spec in minutes. +- **Code generation.** TLA+ specifications describe systems; they are not the system. SpeckDL specifications *become* the system through WASM and TypeScript compilation. + +**When to use TLA+ instead of SpeckDL:** When you need exhaustive model checking for safety-critical algorithms (e.g., verifying a new consensus protocol before implementing it) and don't need production code artifacts or supply chain evidence. + +#### PlusCal + +PlusCal is an algorithm language that compiles to TLA+. It provides a more familiar C/Pascal-like syntax over TLA+'s temporal logic. SpeckDL's syntax is closer to PlusCal's spirit — both aim to make formal specification accessible to working programmers — but SpeckDL skips the TLA+ translation layer and compiles directly to runnable code. + +#### Alloy + +Alloy, from MIT's Software Design Group, is a lightweight formal specification language based on first-order relational logic. It excels at finding counterexamples to structural constraints using its built-in SAT solver. + +**Contrast with SpeckDL:** +- Alloy models *structure* (relationships between entities); SpeckDL models *behavior* (state transitions over time). Alloy is ideal for data model validation. SpeckDL is ideal for protocol and state machine validation. +- Alloy's Alloy Analyzer finds counterexamples within bounded scopes. SpeckDL generates runtime guards that prevent invariant violations in unbounded execution. +- Alloy has no concept of compilation to production code. Its output is visualization and counterexample discovery. + +**Complementary use:** Alloy for data model design + SpeckDL for behavioral specification would cover structural and temporal correctness in a single toolchain. + +### 7.2 Theorem Provers and Verification Systems + +#### Coq / Rocq + +Coq is an interactive theorem prover for dependent type theory. It can express and prove arbitrary mathematical theorems, including program correctness properties. Coq has been used to verify compilers (CompCert C compiler), operating system kernels (seL4 microkernel), and cryptographic libraries. + +**Contrast with SpeckDL:** +- Coq requires proof construction by a human expert. Specifying a consensus protocol in Coq and proving its safety properties is a months-long research effort. SpeckDL expresses the same protocol in ~200 lines with runtime-enforced invariants — a one-day effort. +- Coq's extraction mechanism can generate OCaml, Haskell, or Scheme code from verified specifications. SpeckDL generates TypeScript and WASM directly from uncompromised specifications. +- Coq proves properties statically; SpeckDL enforces them dynamically. Both approaches are valid; they differ in cost and coverage. + +**When to use Coq instead of SpeckDL:** When you need machine-checked proofs of correctness (e.g., a cryptographic primitive, a verified compiler, a microkernel) and can afford the engineering investment. + +#### Dafny + +Dafny is a verification-aware programming language from Microsoft Research that compiles to C#, Java, Go, and JavaScript. It supports preconditions, postconditions, and loop invariants verified by the Z3 SMT solver. + +**Contrast with SpeckDL:** +- Dafny is a *programming language with verification*. SpeckDL is a *specification language with compilation*. In Dafny, you write verified code. In SpeckDL, you write a specification that generates code. +- Dafny's verification is static (Z3 proves properties at compile time). SpeckDL's verification is dynamic (runtime guards at execution time). +- Dafny requires learning verification constructs (ensures clauses, ghost variables, framing). SpeckDL uses conventional guard expressions (`require balance >= amount`). +- Dafny compiles to general-purpose languages. SpeckDL compiles to state machine runtimes optimized for the spec's structure. + +**Overlap:** Both generate verified code from specifications. SpeckDL trades Dafny's static proof power for lower entry cost, automatic provenance generation, and a focus on state-machine-shaped problems. + +### 7.3 Model-Based Design Tools + +#### Event-B + +Event-B is a formal method for system-level modeling and analysis, built on set theory and first-order logic. It uses refinement (starting from abstract models and adding detail) and has been used in railway signaling, automotive, and aerospace systems. + +**Contrast with SpeckDL:** +- Event-B refinement is powerful but requires formal methods expertise. SpeckDL skips refinement and lets you write directly at the level of detail you need. +- Event-B's Rodin platform provides an Eclipse-based IDE with provers. SpeckDL deliberately stays IDE-agnostic (plain text, CLI tooling). +- Event-B does not generate production code or supply chain artifacts. + +#### UML/SysML State Machines + +UML state machine diagrams and SysML behavioral models are the most widely deployed specification tools in industry — and the least useful for runtime safety. They describe behavior visually but cannot be compiled, verified, or audited. SpeckDL fills the gap between a whiteboard diagram and a running system with verifiable properties. + +### 7.4 Code Generation and Specification-as-Code + +#### OpenAPI / gRPC / Protocol Buffers + +Interface definition languages (IDLs) like OpenAPI, Protocol Buffers, and gRPC generate client-server code from API specifications. They solve the same *intent* problem (write a spec once, generate code from it), but at the API surface rather than the behavioral core. + +**Contrast with SpeckDL:** +- IDLs define *interfaces* (what messages look like, what endpoints exist). SpeckDL defines *behavior* (what state exists, how it changes, what must remain true). +- An OpenAPI spec describes your REST API. A SpeckDL spec describes your business logic. They are complementary layers. + +#### P (Microsoft) + +P is a domain-specific language from Microsoft for modeling asynchronous event-driven systems. It compiles to C and integrates with systematic testing to find bugs. P has been used extensively within Microsoft for USB drivers, Azure IoT Hub, and Windows kernel components. + +**Contrast with SpeckDL:** +- P models asynchronous message-passing systems with explicit send/receive semantics. SpeckDL models state machines with implicit concurrency (non-deterministic action interleaving). +- P's systematic testing (bug-finding through state exploration) is analogous to TLA+'s model checking. SpeckDL's runtime invariant enforcement is the complement: catches the bugs in production, not just in testing. +- P compiles to C. SpeckDL compiles to TypeScript and WASM. Both aim for production deployment, but from different modeling paradigms. + +#### Quickstrom + +Quickstrom is a specification language for web applications that checks behavioral properties through property-based testing. It shares SpeckDL's "write a spec, verify behavior" philosophy but targets browser automation rather than state machine compilation. + +### 7.5 SBOM and Supply Chain Tools + +#### Syft / Grype (Anchore) + +Syft generates SBOMs from existing codebases by scanning dependencies. Grype scans those SBOMs for known vulnerabilities. These are *discovery* tools — they tell you what's already in your software. + +**Contrast with SpeckDL:** Speckl doesn't scan. It generates. The SBOM is not an after-the-fact discovery — it is a deliberate artifact of the compilation process. Every generated CycloneDX and SPDX document is accurate by construction, not accurate by scanning. + +#### SLSA Framework + +The Supply-chain Levels for Software Artifacts (SLSA) framework defines four levels of supply chain integrity. SpeckDL contributes to SLSA Level 2+ by: +- Producing verifiable provenance (PROV-O) +- Attaching build metadata to every artifact +- Making the compiler version and commit hash part of the audit trail + +#### in-toto + +in-toto is a framework for securing the software supply chain through cryptographically signed metadata. Speckl's provenance artifacts are complementary: the PROV-O, CycloneDX, and SPDX documents Speckl generates can be signed and verified through in-toto attestations. + +### 7.6 Positioning Summary + +| Tool | Spec Type | Verification | Code Gen | SBOM | Learning Curve | +|------|-----------|-------------|----------|------|----------------| +| **TLA+** | Temporal logic | Model checking (TLC) | None | None | High (weeks) | +| **Alloy** | Relational logic | SAT solving (bounded) | None | None | Medium (days) | +| **Coq/Rocq** | Dependent types | Interactive proofs | Extraction (OCaml/Haskell) | None | Very High (months) | +| **Dafny** | Imperative + specs | SMT (Z3) | C#, Java, Go, JS | None | High (weeks) | +| **Event-B** | Set theory | Proof obligations (Rodin) | None | None | High (weeks) | +| **P (Microsoft)** | State machines | Systematic testing | C | None | Medium (days) | +| **SpeckDL** | State machines | Runtime guards | TypeScript + WASM | Yes (3 formats) | Low (hours) | + +SpeckDL is not a replacement for any of these tools. It occupies a deliberately unfilled niche: **specification language with compiler-level provenance, designed for teams that need evidence of correctness more than proof of correctness.** + +TLA+ proves your algorithm works. Coq proves your implementation matches your spec. SpeckDL *produces* the evidence that connects your spec to your running system, in formats auditors and regulators understand, with a learning curve measured in hours, not weeks. ## 8. Future Work and Roadmap