From 7297b5ec58ca81a0b805c81b0da317856c27f9c5 Mon Sep 17 00:00:00 2001 From: Scott Scoble Date: Tue, 28 Apr 2026 09:33:48 -0700 Subject: [PATCH] feat: whitepaper sections 2-6, README overhaul, SpeckDL spec v0.1, reference agent scaffold - Dark Provenance whitepaper: complete sections 2-6 (What Is Dark Provenance, The Speckl Approach, Semantic Preservation & SA-11, Implications, Call to Action) - README: public launch-ready with architecture, roadmap, getting started - SpeckDL SPEC.md: v0.1 language specification with EBNF grammar, type system, compilation pipeline, 5 example Specks - Reference agent: TypeScript scaffold with Orchestrator, TeamLead, SMEs (VerificationSME, CodegenSME), TillDone condition tracking, ProvenanceGraph, and CLI with example Specks --- README.md | 118 ++++-- docs/whitepapers/dark-provenance.md | 241 +++++++++++- reference-agent/.gitkeep | 0 reference-agent/README.md | 117 ++++++ reference-agent/package.json | 22 ++ reference-agent/src/cli.ts | 180 +++++++++ reference-agent/src/orchestrator.ts | 185 +++++++++ reference-agent/src/provenance.ts | 92 +++++ reference-agent/src/sme.ts | 76 ++++ reference-agent/src/smes/codegen-sme.ts | 142 +++++++ reference-agent/src/smes/verification-sme.ts | 104 +++++ reference-agent/src/team-lead.ts | 122 ++++++ reference-agent/src/till-done.ts | 73 ++++ reference-agent/src/types.ts | 157 ++++++++ reference-agent/tsconfig.json | 24 ++ speckdl/SPEC.md | 389 +++++++++++++++++++ 16 files changed, 2016 insertions(+), 26 deletions(-) delete mode 100644 reference-agent/.gitkeep create mode 100644 reference-agent/README.md create mode 100644 reference-agent/package.json create mode 100644 reference-agent/src/cli.ts create mode 100644 reference-agent/src/orchestrator.ts create mode 100644 reference-agent/src/provenance.ts create mode 100644 reference-agent/src/sme.ts create mode 100644 reference-agent/src/smes/codegen-sme.ts create mode 100644 reference-agent/src/smes/verification-sme.ts create mode 100644 reference-agent/src/team-lead.ts create mode 100644 reference-agent/src/till-done.ts create mode 100644 reference-agent/src/types.ts create mode 100644 reference-agent/tsconfig.json create mode 100644 speckdl/SPEC.md diff --git a/README.md b/README.md index 10d95fa..7305378 100644 --- a/README.md +++ b/README.md @@ -1,44 +1,112 @@ # Speckl -**Spec-first. Everything else follows.** +**Spec-first development with dark provenance.** Write what your system should do. Prove it. Ship with full traceability. -Speckl is an open standard and development system for **spec-first multi-agent development** — define what your software should do in a formal, machine-readable spec, then let AI agents generate, verify, and maintain the implementation. - -## What Makes Speckl Different - -Most dev tools start with code. Speckl starts with the **spec** — a formal, versioned, verifiable contract that lives alongside your code. This contract is the single source of truth. Everything else (tests, docs, implementations, verifications) is derived, checked, and regenerated from it. +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. ## Dark Provenance -Speckl is built on **Dark Provenance** — a methodology for tracking the intent, decisions, and constraints behind every line of generated code. Dark Provenance makes AI-generated software auditable, explainable, and trustworthy by preserving the reasoning chain from spec to implementation. +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. -> *"If you can't trace why every line exists, you don't own your code."* +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. -See the [Dark Provenance Whitepaper](docs/whitepaper.md) for the full methodology. +## SpeckDL -## Strategy - -For the full strategic context and roadmap, read the [Speckl Strategy v2](https://os.scoble.me/forgejo/sscoble/speckl/raw/branch/main/speckl-strategy-v2.md) (or see `speckl-strategy-v2.md` in the workspace). - -## Repository Structure +SpeckDL is the specification language at the core of Speckl. It defines *what* a system does, not *how*: ``` -speckl/ -├── speckdl/ # Speckl Definition Language — the formal spec language -├── reference-agent/ # Reference implementation of a Speckl-compliant agent -├── docs/ # Documentation and whitepapers -├── examples/ # Example specs and generated outputs -└── LICENSE # MIT License +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)) +} ``` -## Status +SpeckDL compiles through a deterministic pipeline: -**Early / Pre-Alpha** — The spec language is being drafted. Nothing is stable. Contributions and feedback are welcome. +``` +SpeckDL ──► Z3 (SMT solver) ──► DST (decision structures) ──► WASM + │ │ │ │ + │ verify constraints compile to decision deploy verified + │ catch contradictions trees artifacts + │ + └── Provenance graph grows automatically at each stage +``` -## Parent +No LLMs in the compilation path. No non-determinism. Same input, same output — every time. -**Greybeard Holdings, LLC** — bootstrapped, independent, Scott Scoble, CEO. +## Architecture + +``` +┌─────────────────────────────────────────────────┐ +│ Orchestrator │ +│ Accepts Specks, decomposes tasks │ +└───────────┬─────────────────┬───────────────────┘ + │ │ + ┌───────▼───────┐ ┌───────▼───────┐ + │ Team Lead │ │ Team Lead │ + │ Verification │ │ Codegen │ + └───────┬───────┘ └───────┬───────┘ + │ │ + ┌───────▼───────┐ ┌───────▼───────┐ + │ Z3 SME │ │ TypeScript │ + │ (verify) │ │ SME (emit) │ + └───────────────┘ └───────────────┘ +``` + +- **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. + +## 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 +npm install +npm run dev +``` + +## Roadmap + +Speckl follows a phased strategy — the open standard fuels everything else: + +| Phase | Focus | Timeline | +|-------|-------|----------| +| **D — Open Standard** | SpeckDL language, Dark Provenance methodology, reference implementations | Now → 3mo | +| **C — Consulting** | Hands-on engagements with regulated-industry teams, validating the methodology | Now → 3mo (funds D) | +| **A — Developer Tool (SaaS)** | Self-serve platform: spec editor, live Z3 verification, provenance graph browser | 3 → 9mo | +| **B — Compliance API** | Enterprise provenance engine: audit reports, traceability matrices, compliance packs | 9 → 18mo | + +The standard comes first. Adoption creates the market. The products follow. + +## Contributing + +Speckl is open source under the [MIT license](LICENSE). We welcome contributions: + +- **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 + +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. ## License -MIT — see [LICENSE](LICENSE). +MIT © Scott Scoble / Greybeard Holdings, LLC \ No newline at end of file diff --git a/docs/whitepapers/dark-provenance.md b/docs/whitepapers/dark-provenance.md index aa6e220..58a6f99 100644 --- a/docs/whitepapers/dark-provenance.md +++ b/docs/whitepapers/dark-provenance.md @@ -70,4 +70,243 @@ We need dark provenance. --- -*Next section: **What Is Dark Provenance** — A methodology where every behavior traces back to its original source, invisible until needed, but always present.* +## Section 2: What Is Dark Provenance + +Dark provenance is a methodology for software development where every behavior in a system — every function, every branch, every side effect — is traced back to its original source of intent. That source might be an academic paper describing an algorithm, a regulatory clause in DO-178C Annex A, a design decision captured in an architecture review, or a human conversation where a product owner said "we need this." + +The word "dark" does not mean hidden or malicious. It means *ambient*. Like dark matter, it's always present, shaping the structure of the system, but you don't observe it directly until you go looking. The provenance graph exists from the moment a specification is written; it grows as the system is implemented; and it can be materialized on demand — for an audit, for a compliance report, or for a developer who asks "why is this here?" + +**How it differs from traditional traceability.** + +Conventional traceability links requirements to code through a chain of documents: requirement → design spec → code module → test case. This works when the chain is hand-maintained and all artifacts are human-authored. It breaks when LLMs generate code that bypasses the document chain. + +Dark provenance inverts the model. Instead of *forward-tracing* from documents to code, it *backward-traces* from every runtime behavior to the specification that motivated it. The specification is the primary artifact — not the code. Code is a derived artifact, generated (or verified) against the spec. + +This creates a fundamental asymmetry that works in our favor: specifications are small, human-readable, and stable. Code is large, machine-generated or machine-verified, and frequently regenerated. By anchoring provenance to the spec, we make the audit surface tractable regardless of how much code the system contains. + +**The provenance graph.** + +A dark provenance system maintains a directed graph where: + +- **Nodes** are sources of intent: specifications, regulatory requirements, design decisions, constraints, verification results. +- **Edges** are derivation relationships: "spec A was decomposed into sub-specs B and C," "code module X was generated from spec A," "test case T verifies constraint K from spec A." +- **Each edge carries metadata:** who created it, when, what tool was used, what verification was performed. + +The graph is *incremental*. It grows as the system evolves. It is *queryable*: "Show me every behavior derived from DO-178C section 6.3" is a graph traversal, not a manual search through Jira. + +**Why "dark" matters.** + +The key design decision is that the provenance graph is maintained *automatically* by the toolchain. Developers don't write provenance metadata by hand. The specification language (SpeckDL) encodes intent directly. The compilation pipeline records derivation edges automatically. The agent harness tags generated code with its source spec. + +This means developers work with specifications, not with traceability documents. The provenance is dark — it accumulates behind the scenes. It becomes visible only when someone needs it: an auditor, a compliance officer, or a developer debugging a production incident. + +**The analogy to financial accounting.** + +Think of it like double-entry bookkeeping. Every financial transaction creates two entries that must balance. The system doesn't prevent fraud, but it makes fraud *detectable* and *traceable*. Dark provenance does the same for software intent. Every behavior must have a source. The system doesn't prevent bugs, but it makes every behavior's origin *traceable*. + +No one argues that double-entry bookkeeping is too much overhead for a startup. It's just how accounting works. Dark provenance should be just how software development works — especially when AI agents are writing the code. + +--- + +## Section 3: The Speckl Approach + +Speckl implements dark provenance through three interlocking mechanisms: a specification language (SpeckDL), a formal verification pipeline, and a tiered agent architecture. + +**SpeckDL: The specification language.** + +SpeckDL is a domain-specific language for defining system behavior and interfaces. A SpeckDL specification (a "Speck") describes *what* a system should do, not *how* it should do it. Key constructs include: + +- **Speck definitions:** Named behavioral units with typed inputs, outputs, and constraints. +- **Interfaces:** Contracts between Specks — what one Speck expects from another. +- **Constraints:** Invariants, preconditions, postconditions, and temporal properties expressed in a form compilable to Z3 (an SMT solver). +- **Verification boundaries:** Explicit markers indicating where human review is required versus where automated verification suffices. + +A Speck is intentionally small — typically 20-80 lines. It captures a single behavioral unit at a level of abstraction that humans can read and reason about directly. Here is a simplified example: + +``` +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)) +} +``` + +This Speck says: the retry handler takes an operation and a maximum retry count; retries may not exceed 5; delay doubles on each retry; total delay is bounded to 30 seconds; and the verifier must prove that every retry after the first has a positive delay. The implementation — the code that satisfies these constraints — is a derived artifact. + +**The verification pipeline.** + +SpeckDL compiles through a deterministic pipeline: + +1. **SpeckDL → Z3:** Constraints and verification conditions are compiled into SMT-LIB format for the Z3 solver. If Z3 reports UNSAT, the Speck contains contradictory constraints — it's impossible to implement correctly. +2. **Z3 → DST (Decision Structures):** Z3's model is compiled into DSTs — deterministic decision trees that map inputs to verified outputs. DSTs represent the complete behavioral space of a verified Speck. +3. **DST → WASM:** DSTs compile to WebAssembly, producing an executable artifact that is *provably correct by construction* — it implements exactly the behaviors the Speck specifies, no more and no less. + +This pipeline is deterministic. Given the same Speck, the same Z3 version, and the same compilation flags, it produces the same output. There is no non-determinism, no hallucination, no model variance. This property is essential for auditability. + +**The tiered agent harness.** + +Not all code can be generated from verified Specks. Real systems include glue code, integrations, UIs, and infrastructure that don't warrant formal specification. For these, Speckl provides a tiered agent architecture: + +- **Orchestrator:** The client entry point. Accepts a Speck (or a natural language request), decomposes it into verification tasks, and assigns them to Team Leads. +- **Team Leads:** Manage specialized agents. A Team Lead for verification tasks routes Specks to the Z3 pipeline. A Team Lead for code generation routes verified DSTs to codegen agents. A Team Lead for integration routes glue-code tasks to appropriate SMEs. +- **SMEs (Subject Matter Experts):** Hyper-specialized single-task agents. A verification SME runs Z3. A codegen SME produces TypeScript or Rust from a DST. A documentation SME produces human-readable docs from the provenance graph. + +Teams self-replicate: if a Team Lead's queue is saturated, it can request the Orchestrator to spawn another Team Lead of the same type. This gives the system elastic scaling without human intervention. + +**TillDone: Condition-based task tracking.** + +Traditional task trackers use status fields: "to do," "in progress," "done." Speckl replaces this with TillDone, a condition-based model. A task is not "done" when someone moves a card. A task is done when a *provable condition* is met: Z3 returns SAT, all generated code passes the test suite, the provenance graph is complete for this Speck. + +This eliminates the most common failure mode in traditional traceability: the gap between "marked done" and "actually verified." In TillDone, the verification *is* the completion condition. + +--- + +## Section 4: Semantic Preservation and SA-11 (RTCA DO-178C) + +The most consequential application of dark provenance is in software assurance — specifically, in satisfying the intent of standards like RTCA DO-178C, IEC 62304, and ISO 26262 without the crushing cost of current compliance methods. + +**The review boundary problem.** + +DO-178C (and its European counterpart ED-12C) defines five levels of software assurance (DAL A through E). At the highest levels (DAL A and B), every line of code must be traceable to a requirement, verified against a test case, and reviewed by an independent assessor. For a modern codebase of hundreds of thousands of lines, this is enormously expensive — often 40-60% of total project cost. + +The core challenge is the *review boundary*: where does human review happen? Current practice reviews code directly, line by line. This made sense when humans wrote every line. It makes no sense when an agent generates code from a verified specification. + +**The Speck review boundary.** + +Speckl proposes a different review boundary: **humans review Specks, not generated code.** This is defensible if and only if the compilation pipeline preserves semantics — that is, if the WASM artifact produced from a verified Speck implements exactly the behaviors the Speck specifies. + +This property is called *semantic preservation*. If it holds, then: + +1. Human review at the Speck boundary ensures that *intent* is correct. +2. The Z3 verification ensures that the Speck is *internally consistent* (no contradictions, all constraints satisfiable). +3. The deterministic compilation ensures that the *implementation matches the spec*. +4. The provenance graph provides the *traceability evidence* that auditors require. + +The combination of (1)-(4) satisfies the *intent* of DO-178C's traceability objectives (Annex A, Tables A-2 through A-6) without requiring line-by-line code review. + +**What semantic preservation requires.** + +Semantic preservation is not automatic. It requires: + +- A *formally defined* specification language with unambiguous semantics. SpeckDL must have a denotational semantics that maps every construct to a mathematical object. +- A *verified compiler* that preserves those semantics through each compilation stage. This is the hardest engineering challenge in Speckl. The compiler must be small enough to audit, and its correctness must be verified (potentially by a different verification tool — a bootstrapping problem we discuss below). +- *Deterministic compilation.* Given the same input, the compiler must always produce the same output. No randomness, no heuristics, no LLM in the compilation path. + +The last point is critical and often misunderstood. Speckl uses LLMs for code generation in the *agent harness* — for glue code, UIs, and other non-critical paths. But the formal compilation pipeline (SpeckDL → Z3 → DST → WASM) contains no LLMs. It is purely deterministic. This is non-negotiable for semantic preservation. + +**The bootstrapping problem.** + +To trust the compiler, you must verify it. But the compiler is a program — verifying it requires a verification tool, which itself must be trusted. This is the classic bootstrapping problem in formal methods. + +Speckl's approach is pragmatic, not purist: + +1. The compiler is kept as small as possible — ideally under 5,000 lines of TypeScript. +2. The compiler is tested against a comprehensive suite of property-based tests. +3. The Z3 integration is the most trusted component — Z3 itself is extensively verified by Microsoft Research. +4. The DST and WASM codegen stages are simple enough for manual review. +5. As the Speckl ecosystem matures, the compiler can be formally verified using tools like Coq or Lean — but this is a Phase 3 objective, not a launch requirement. + +**Implications for other standards.** + +The same reasoning applies to other software assurance standards: + +- **IEC 62304** (medical device software): Requires traceability from software requirements through unit tests. Dark provenance provides this automatically. +- **ISO 26262** (automotive functional safety): Requires demonstration that safety requirements are met. Verified Specks with semantic preservation provide stronger evidence than test-based verification alone. +- **SOC 2 / FedRAMP** (information security): Require evidence of change management and access controls. The provenance graph provides an immutable record of every change, its source, and its verification status. + +In each case, the argument is the same: if humans review the specification, and the compilation pipeline preserves semantics, then the generated implementation inherits the specification's assurance properties. This is not a loophole — it's a stronger guarantee than current practice provides. + +--- + +## Section 5: Implications for AI-Augmented Development + +Dark provenance does not merely solve a compliance problem. It changes the economics of AI-augmented software development. + +**The trust ceiling.** + +Today, there is a trust ceiling on AI-generated code. Organizations adopt LLMs for autocomplete, boilerplate, and internal tooling — low-stakes contexts where bugs are acceptable. For production systems, safety-critical code, and regulated environments, LLMs are excluded or heavily constrained. + +This ceiling exists because we cannot verify LLM output. We can test it, review it, and monitor it in production — but we cannot *prove* it correct. Testing is probabilistic; formal verification is categorical. Dark provenance, combined with the Speckl verification pipeline, moves AI-generated code from the probabilistic regime to the categorical regime. + +**The provenance graph as competitive advantage.** + +Organizations that adopt dark provenance accumulate a provenance graph — a detailed, queryable record of every decision, specification, and verification in their system's history. This graph becomes a strategic asset: + +- **Onboarding:** New engineers can query the graph to understand why any piece of code exists, without relying on tribal knowledge. +- **Audit readiness:** Compliance evidence is always available, not assembled under deadline pressure. +- **Risk assessment:** The graph makes it trivial to identify which behaviors are affected by a change to a requirement, a regulation, or a design decision. +- **Insurance and liability:** Insurers and legal teams can evaluate software risk based on provenance coverage rather than guesswork. + +No organization that has built a provenance graph will want to operate without one. This creates natural lock-in — the good kind, where staying is genuinely better than leaving. + +**Agent economics.** + +The tiered agent architecture changes the cost structure of software development. Today, the bottleneck is human review: humans must review AI-generated code, and this review capacity doesn't scale. In Speckl, the bottleneck moves to *specification authoring* — writing Specks is creative, intellectual work that humans do well and enjoy. The rest — verification, code generation, integration, documentation — is handled by agents operating within a verified framework. + +This doesn't eliminate human work. It shifts it from review (low-value, error-prone, unscalable) to specification (high-value, creative, inherently human). The humans who used to spend 40% of their time reviewing AI-generated code can now spend that time on the work that matters: defining what the system should do, and why. + +**The spectrum of formality.** + +Not everything needs a verified Speck. A CRUD endpoint for an internal admin tool doesn't need Z3 verification. A patient monitoring system does. Dark provenance supports a spectrum: + +- **Verified Specks** (full pipeline): For safety-critical and regulated behaviors. Z3-verified, DST-compiled, WASM-deployed. Full provenance graph. +- **Verified-by-test Specks** (spec + tests): For important but non-critical behaviors. Human-authored spec, human-written or agent-generated code, test-verified. Provenance graph links spec to code and tests. +- **Unspecified code** (agent-generated): For glue code, UIs, and low-stakes infrastructure. Agent-generated, human-reviewed. Provenance graph records that the code was generated by an agent without a formal spec. + +This spectrum is crucial for adoption. Teams can start with unspecified code, adopt verified-by-test Specks for their most important behaviors, and move to fully verified Specks as confidence and compliance needs grow. Dark provenance is not an all-or-nothing methodology. + +**The future: agents that prove, not just produce.** + +The deepest implication is this: dark provenance enables a future where AI agents don't just generate code — they generate *verified* code. Not code that might work. Code that provably satisfies a specification. + +This is a qualitative shift. Today's AI coding agents are productivity tools: they make developers faster. Tomorrow's verified agents are assurance tools: they make software trustworthy. The difference between "this code was generated by an AI" and "this code was proven correct against its specification" is the difference between a productivity claim and a trust guarantee. + +Dark provenance is the methodology that makes this shift possible. Without it, AI-generated code will always hit the trust ceiling. With it, agents become the most trusted participants in the software development process — because their output is verified, not just reviewed. + +--- + +## Section 6: Call to Action + +The software industry faces a choice. AI agents will generate an increasing share of production code — this is certain. What's uncertain is whether we'll be able to trust that code. + +Without a methodology for tracing intent, we're heading toward a world where most software is written by machines and understood by no one. Compliance becomes theater. Audits become approximations. And when something goes wrong — when an AI-generated system fails in a safety-critical context — we'll have no way to answer the most basic question: *why did it do that?* + +Dark provenance is the alternative. It's not a product. It's not a framework. It's a methodology: capture intent before code, maintain provenance automatically, and verify behavior formally. The tools that implement this methodology — SpeckDL, the verification pipeline, the agent harness — are means, not ends. + +**What you can do today.** + +1. **Adopt specification-first development.** Before you write code — or prompt an LLM to write code — write a specification. Even an informal one. Make the spec the primary artifact, not the code. This single practice, adopted widely, would dramatically improve traceability in AI-augmented systems. + +2. **Make provenance a first-class artifact.** Treat the provenance graph like you treat your test suite: something that grows with the system, runs in CI, and blocks deployment if it's incomplete. The graph doesn't have to be formal at first. Start with links between requirements, specs, and code. Make it queryable. Make it automatic. + +3. **Contribute to Speckl.** The SpeckDL language spec and reference implementation are open source (MIT license). We need: + - Language designers to help refine SpeckDL's syntax and semantics + - Formal methods engineers to work on the verified compiler + - Domain experts in DO-178C, IEC 62304, and ISO 26262 to validate the compliance model + - Agent developers to build and test the tiered agent harness + - Writers and educators to make dark provenance accessible to working developers + +4. **Talk to your compliance team.** If you work in a regulated industry, show them this paper. Ask: "What would it take to prove — not just demonstrate — that our software satisfies its requirements?" The answer to that question is the starting point for dark provenance adoption. + +5. **Publish your provenance.** If you adopt specification-first development, share your specs. Share your provenance graphs. Make the methodology visible. The more teams that practice dark provenance, the more valuable the methodology becomes for everyone. + +**The standard is the strategy.** + +Dark provenance is not proprietary. SpeckDL is not a moat. The Speckl project's commercial viability depends on *adoption*, not exclusion. We build the standard, publish the methodology, and let the market find us. The consulting, the SaaS, the compliance API — these are consequences of adoption, not prerequisites. + +This is an unusual strategy for a startup. Most startups build a product, find customers, and grow. Speckl builds a standard, finds practitioners, and grows. The difference matters because standards compound: every team that adopts SpeckDL makes the ecosystem more valuable for every other team. Every provenance graph that exists makes the case for dark provenance stronger. + +The software industry didn't adopt version control because someone sold it to them. They adopted it because it was obviously better than the alternative. Dark provenance is obviously better than the alternative — which is, let's be honest, no provenance at all. + +Join us. Write specs. Build provenance. Make intent traceable. + +--- + +*Scott Scoble is the creator of Speckl and the Dark Provenance methodology. He writes about the human side of software development at scoble.me.* + +*Speckl is open source under the MIT license. Repository: github.com/sscoble/speckl* + +*This whitepaper is a living document. Feedback, corrections, and contributions are welcome at speckl.dev (forthcoming) or via the repository issues.* diff --git a/reference-agent/.gitkeep b/reference-agent/.gitkeep deleted file mode 100644 index e69de29..0000000 diff --git a/reference-agent/README.md b/reference-agent/README.md new file mode 100644 index 0000000..17f007a --- /dev/null +++ b/reference-agent/README.md @@ -0,0 +1,117 @@ +# Speckl Reference Agent Architecture + +A working reference implementation of the Speckl tiered agent architecture: Orchestrator → Team Lead → SME, with TillDone condition-based task tracking and dark provenance. + +## Architecture + +``` +┌─────────────────────────────────────────────────┐ +│ Orchestrator │ +│ Accepts Specks, decomposes tasks │ +└───────────┬─────────────────┬───────────────────┘ + │ │ + ┌───────▼───────┐ ┌───────▼───────┐ + │ Team Lead │ │ Team Lead │ + │ Verification │ │ Codegen │ + └───────┬───────┘ └───────┬───────┘ + │ │ + ┌───────▼───────┐ ┌───────▼───────┐ + │ Z3 SME │ │ TypeScript │ + │ (verify) │ │ SME (emit) │ + └───────────────┘ └───────────────┘ +``` + +## Components + +| File | Purpose | +|------|---------| +| `src/types.ts` | Core types: SpeckDefinition, Task, ProvenanceEdge, TillDoneCondition | +| `src/orchestrator.ts` | Orchestrator — accepts Specks, manages pipeline, aggregates results | +| `src/team-lead.ts` | TeamLead + pre-built VerificationTeamLead, CodegenTeamLead | +| `src/sme.ts` | Abstract SME base class | +| `src/smes/verification-sme.ts` | Z3 verification SME (simulated) | +| `src/smes/codegen-sme.ts` | Code generation SME (TypeScript + Rust) | +| `src/till-done.ts` | TillDone — condition-based task tracking | +| `src/provenance.ts` | ProvenanceGraph — dark provenance recording and querying | +| `src/cli.ts` | CLI entry point with example Specks | + +## Quick Start + +```bash +# Install dependencies +npm install + +# Run with example Specks +npx tsx src/cli.ts --speck RetryHandler +npx tsx src/cli.ts --speck RateLimiter +npx tsx src/cli.ts --speck DrugDosageCalculator + +# Show provenance graph +npx tsx src/cli.ts --speck RetryHandler --provenance + +# List available Specks +npx tsx src/cli.ts --list +``` + +## Pipeline Flow + +1. **Orchestrator** receives a Speck definition +2. **Verification phase**: VerificationTeamLead assigns to Z3 SME, which: + - Compiles constraints to SMT-LIB2 + - Invokes Z3 (simulated in reference impl) + - Reports SAT/UNSAT with counterexamples + - Records provenance edge: `speck → z3:verified_by` +3. **Codegen phase**: CodegenTeamLead assigns to Codegen SME, which: + - Generates TypeScript or Rust from the verified Speck + - Emits constraint-check scaffolding + - Records provenance edge: `speck → code:generated_from` +4. **Orchestrator** aggregates results, merges provenance graphs +5. **TillDone** evaluates: each task is done when its proven condition is met + +## TillDone Conditions + +Tasks don't tick boxes — they evaluate predicates: + +```typescript +// Built-in predicates +TillDoneTracker.predicates.z3Verified(result) // Z3 returned SAT +TillDoneTracker.predicates.noContradictions(result) // No contradictory constraints +TillDoneTracker.predicates.codeGenerated(result) // Code was produced +TillDoneTracker.predicates.provenanceComplete(result) // Provenance edges exist +``` + +## Provenance Graph + +Every derivation is recorded: + +```json +{ + "source": "speck:RetryHandler", + "target": "z3:task-1", + "relation": "verified_by", + "tool": "Z3 4.12.5", + "timestamp": "2026-04-28T09:00:00Z", + "metadata": { "constraintCount": 3, "allVerified": true } +} +``` + +The graph is queryable by source, relation, or target. You can trace any artifact back to its origin. + +## Extending + +To add a new SME: + +1. Create a class extending `SME` in `src/smes/` +2. Implement `capabilities` and `execute()` +3. Register it with the appropriate TeamLead +4. The Orchestrator will automatically route matching tasks to it + +To add a new Team Lead: + +1. Create a class extending `TeamLead` +2. Register SMEs in the constructor +3. Register the TeamLead with the Orchestrator + +## License + +MIT © Scott Scoble / Greybeard Holdings, LLC \ No newline at end of file diff --git a/reference-agent/package.json b/reference-agent/package.json new file mode 100644 index 0000000..4eba854 --- /dev/null +++ b/reference-agent/package.json @@ -0,0 +1,22 @@ +{ + "name": "@speckl/reference-agent", + "version": "0.1.0", + "description": "Reference Agent Architecture — Speckl's tiered agent harness", + "private": true, + "type": "module", + "scripts": { + "build": "tsc", + "start": "node dist/cli.js", + "dev": "npx tsx src/cli.ts", + "example": "npx tsx src/cli.ts", + "test": "node --experimental-vm-modules node_modules/.bin/jest" + }, + "engines": { + "node": ">=18" + }, + "devDependencies": { + "@types/node": "^20.0.0", + "typescript": "^5.4.0" + }, + "dependencies": {} +} diff --git a/reference-agent/src/cli.ts b/reference-agent/src/cli.ts new file mode 100644 index 0000000..f90a14e --- /dev/null +++ b/reference-agent/src/cli.ts @@ -0,0 +1,180 @@ +#!/usr/bin/env node +/** + * Speckl Reference Agent — CLI entry point. + * + * Usage: + * npx tsx src/cli.ts examples/ --speck RetryHandler + * npx tsx src/cli.ts --help + */ + +import { Orchestrator } from "./orchestrator.js"; +import type { SpeckDefinition, Constraint, VerifyCondition } from "./types.js"; + +// ─── Example Specks ───────────────────────────────────────── + +const exampleSpecks: Record = { + RetryHandler: { + name: "RetryHandler", + input: { + operation: { kind: "named", name: "Operation" }, + maxRetries: "Nat", + }, + output: { kind: "named", name: "Result" }, + constraints: [ + { id: "c1", expression: "maxRetries <= 5" }, + { id: "c2", expression: "backoff(delay(n)) == delay(n-1) * 2" }, + { id: "c3", expression: "totalDelay < 30s" }, + ] as Constraint[], + verify: [ + { id: "v1", kind: "always", expression: "implies(attempt > 1, delay > 0)" }, + ] as VerifyCondition[], + }, + + RateLimiter: { + name: "RateLimiter", + input: { + requests: { kind: "list", element: { kind: "named", name: "Request" } }, + window: "Nat", + maxRequests: "Nat", + }, + output: { + kind: "record", + fields: { + allowed: { kind: "list", element: "Bool" }, + remaining: "Nat", + }, + }, + constraints: [ + { id: "c1", expression: "maxRequests > 0" }, + { id: "c2", expression: "window > 0" }, + { id: "c3", expression: "count(allowed, true) <= maxRequests" }, + { id: "c4", expression: "remaining == maxRequests - count(allowed, true)" }, + ] as Constraint[], + verify: [ + { id: "v1", kind: "always", expression: "implies(remaining == 0, not(allowed[current]))" }, + ] as VerifyCondition[], + }, + + DrugDosageCalculator: { + name: "DrugDosageCalculator", + input: { + patientWeight: "Real", + drugConcentration: "Real", + prescribedDose: "Real", + minDose: "Real", + maxDose: "Real", + frequency: "Nat", + }, + output: { + kind: "record", + fields: { + volume: "Real", + safe: "Bool", + }, + }, + constraints: [ + { id: "c1", expression: "patientWeight > 0" }, + { id: "c2", expression: "drugConcentration > 0" }, + { id: "c3", expression: "minDose > 0" }, + { id: "c4", expression: "maxDose > minDose" }, + { id: "c5", expression: "frequency >= 1" }, + { id: "c6", expression: "frequency <= 6" }, + { id: "c7", expression: "implies(safe, volume >= minDose / drugConcentration)" }, + { id: "c8", expression: "implies(safe, volume <= maxDose / drugConcentration)" }, + { id: "c9", expression: "implies(not safe, volume == 0)" }, + ] as Constraint[], + verify: [ + { id: "v1", kind: "always", expression: "implies(prescribedDose >= minDose and prescribedDose <= maxDose, safe)" }, + { id: "v2", kind: "always", expression: "implies(not safe, volume == 0)" }, + ] as VerifyCondition[], + events: [ + { + name: "DoseCalculated", + fields: { volume: "Real", safe: "Bool" }, + }, + { + name: "DoseRejected", + fields: { reason: "String" }, + }, + ], + }, +}; + +// ─── Main ──────────────────────────────────────────────────── + +async function main(): Promise { + const args = process.argv.slice(2); + + if (args.includes("--help") || args.includes("-h")) { + console.log(` +Speckl Reference Agent v0.1 + +Usage: + npx tsx src/cli.ts [options] + +Options: + --speck Process a specific example Speck + --list List available example Specks + --provenance Show provenance graph after processing + --help Show this help message + +Example Specks: + ${Object.keys(exampleSpecks).join("\n ")} +`); + return; + } + + if (args.includes("--list")) { + console.log("Available example Specks:"); + for (const [name, speck] of Object.entries(exampleSpecks)) { + console.log(` ${name}: ${speck.constraints.length} constraints, ${speck.verify.length} verify conditions`); + } + return; + } + + const speckName = args[args.indexOf("--speck") + 1] || "RetryHandler"; + const speck = exampleSpecks[speckName]; + + if (!speck) { + console.error(`Unknown Speck: ${speckName}`); + console.error(`Available: ${Object.keys(exampleSpecks).join(", ")}`); + process.exit(1); + } + + console.log(`\n🧬 Processing Speck: ${speck.name}`); + console.log(` Constraints: ${speck.constraints.length}`); + console.log(` Verify conditions: ${speck.verify.length}`); + console.log(` Events: ${speck.events?.length ?? 0}\n`); + + const orchestrator = new Orchestrator(); + const result = await orchestrator.processSpeck(speck); + + console.log(`\n✅ Result: ${result.status}`); + console.log(` Duration: ${result.durationMs}ms`); + + for (const [taskId, taskResult] of Object.entries(result.results)) { + const r = taskResult as any; + console.log(`\n Task ${taskId}: ${r.status}`); + if (r.output) { + if (r.output.z3Result) { + console.log(` Z3 result: ${r.output.z3Result}`); + console.log(` All verified: ${r.output.allVerified ?? "N/A"}`); + } + if (r.output.code) { + console.log(` Generated ${r.output.language} code (${r.output.code.split("\n").length} lines)`); + } + } + } + + if (args.includes("--provenance")) { + console.log(`\n📊 Provenance Graph:`); + console.log(JSON.stringify(result.provenance, null, 2)); + } + + console.log(); +} + +main().catch((err) => { + console.error("Fatal error:", err); + process.exit(1); +}); \ No newline at end of file diff --git a/reference-agent/src/orchestrator.ts b/reference-agent/src/orchestrator.ts new file mode 100644 index 0000000..7a32888 --- /dev/null +++ b/reference-agent/src/orchestrator.ts @@ -0,0 +1,185 @@ +/** + * Orchestrator — Client entry point for the Speckl agent harness. + * + * Accepts Specks, decomposes them into verification and codegen tasks, + * assigns tasks to Team Leads, and aggregates results with full provenance. + */ + +import type { + AgentId, + SpeckDefinition, + Task, + TaskMessage, + TaskResult, + TaskType, + ProvenanceEdge, +} from "./types.js"; +import { TeamLead, VerificationTeamLead, CodegenTeamLead } from "./team-lead.js"; +import { TillDoneTracker } from "./till-done.js"; +import { ProvenanceGraphImpl } from "./provenance.js"; + +export class Orchestrator { + readonly id: AgentId = { type: "orchestrator", name: "speckl-orchestrator" }; + private teamLeads: TeamLead[] = []; + protected provenance: ProvenanceGraphImpl; + protected tillDone: TillDoneTracker; + private taskCounter = 0; + + constructor() { + this.provenance = new ProvenanceGraphImpl(); + this.tillDone = new TillDoneTracker(); + + // Register default teams + this.registerTeamLead(new VerificationTeamLead()); + this.registerTeamLead(new CodegenTeamLead()); + } + + /** Register a Team Lead. */ + registerTeamLead(lead: TeamLead): void { + this.teamLeads.push(lead); + } + + /** + * Process a Speck through the full pipeline: + * 1. Verify constraints (Z3) + * 2. Generate code (TypeScript/Rust) + * 3. Return aggregated results with provenance graph + */ + async processSpeck(speck: SpeckDefinition): Promise { + const startTime = Date.now(); + const results: Map = new Map(); + + // Record speck in provenance graph + this.provenance.addNode({ + id: `speck:${speck.name}`, + type: "speck", + label: speck.name, + metadata: { + constraintCount: speck.constraints.length, + verifyCount: speck.verify.length, + importedAt: new Date().toISOString(), + }, + }); + + // Phase 1: Verification + const verifyTask = this.createTask(speck.name, "verify_speck", `Verify Speck ${speck.name} constraints`, 1); + this.tillDone.register(verifyTask.id, `Z3 verifies ${speck.name}`, TillDoneTracker.predicates.z3Verified); + + const verifyLead = this.findTeamForTask(verifyTask); + if (!verifyLead) { + return this.fail(speck.name, "No verification team available", startTime); + } + + const verifyResult = await verifyLead.handleAssignment( + this.createAssignment(verifyTask, speck), + speck + ); + results.set(verifyTask.id, verifyResult); + this.mergeProvenance(verifyResult.provenance); + + if (verifyResult.status !== "success") { + return this.fail(speck.name, "Verification failed", startTime, results); + } + + // Phase 2: Code generation + const codegenTask = this.createTask(speck.name, "generate_code", `Generate code for ${speck.name}`, 2, verifyTask.id); + this.tillDone.register(codegenTask.id, `Code generated for ${speck.name}`, TillDoneTracker.predicates.codeGenerated); + + const codegenLead = this.findTeamForTask(codegenTask); + if (!codegenLead) { + return this.fail(speck.name, "No codegen team available", startTime, results); + } + + const codegenResult = await codegenLead.handleAssignment( + this.createAssignment(codegenTask, speck), + speck + ); + results.set(codegenTask.id, codegenResult); + this.mergeProvenance(codegenResult.provenance); + + const allDone = this.tillDone.completed().length === 2; + + return { + speckName: speck.name, + status: allDone ? "success" : "partial", + results: Object.fromEntries(results), + provenance: this.provenance.toJSON(), + durationMs: Date.now() - startTime, + }; + } + + /** Create a new task. */ + private createTask( + speckName: string, + taskType: TaskType, + description: string, + priority: number, + parentTaskId?: string + ): Task { + return { + id: `task-${++this.taskCounter}`, + speckName, + taskType, + description, + priority, + parentTaskId, + createdAt: new Date().toISOString(), + }; + } + + /** Create an assignment message for a Team Lead. */ + private createAssignment(task: Task, speck: SpeckDefinition): TaskMessage { + return { + id: `msg-${task.id}`, + type: "task_assign", + from: this.id, + to: { type: "team_lead", name: "auto" }, + payload: { task, speck }, + timestamp: new Date().toISOString(), + provenance: [], + }; + } + + /** Find a Team Lead that can handle the given task. */ + private findTeamForTask(task: Task): TeamLead | undefined { + return this.teamLeads.find((lead) => lead.canHandle(task)); + } + + /** Merge provenance edges from a result. */ + private mergeProvenance(edges: ProvenanceEdge[]): void { + for (const edge of edges) { + this.provenance.addEdge(edge); + } + } + + /** Build a failure result. */ + private fail( + speckName: string, + reason: string, + startTime: number, + partialResults?: Map + ): OrchestrationResult { + return { + speckName, + status: "failure", + results: partialResults ? Object.fromEntries(partialResults) : {}, + provenance: this.provenance.toJSON(), + durationMs: Date.now() - startTime, + error: reason, + }; + } + + /** Get the full provenance graph. */ + getProvenance(): object { + return this.provenance.toJSON(); + } +} + +export interface OrchestrationResult { + speckName: string; + status: "success" | "partial" | "failure"; + results: Record; + provenance: object; + durationMs: number; + error?: string; +} \ No newline at end of file diff --git a/reference-agent/src/provenance.ts b/reference-agent/src/provenance.ts new file mode 100644 index 0000000..3f191ab --- /dev/null +++ b/reference-agent/src/provenance.ts @@ -0,0 +1,92 @@ +/** + * ProvenanceGraph — Dark provenance tracking for the Speckl agent harness. + * + * Records every derivation edge in the compilation pipeline. + * Queryable by source, relation, or target. + */ + +import type { ProvenanceEdge, ProvenanceNode } from "./types.js"; + +export class ProvenanceGraphImpl { + private nodes: Map = new Map(); + private edges: ProvenanceEdge[] = []; + + addNode(node: ProvenanceNode): void { + this.nodes.set(node.id, node); + } + + addEdge(edge: ProvenanceEdge): void { + this.edges.push(edge); + } + + query( + source?: string, + relation?: string, + target?: string + ): ProvenanceEdge[] { + return this.edges.filter((edge) => { + if (source && edge.source !== source) return false; + if (relation && edge.relation !== relation) return false; + if (target && edge.target !== target) return false; + return true; + }); + } + + /** Trace all edges from a source (transitive). */ + traceFrom(sourceId: string): ProvenanceEdge[] { + const visited = new Set(); + const result: ProvenanceEdge[] = []; + const queue = [sourceId]; + + while (queue.length > 0) { + const current = queue.pop()!; + if (visited.has(current)) continue; + visited.add(current); + + const outgoing = this.query(current); + for (const edge of outgoing) { + result.push(edge); + queue.push(edge.target); + } + } + + return result; + } + + /** Get all nodes reachable from a source. */ + reachableFrom(sourceId: string): ProvenanceNode[] { + const edges = this.traceFrom(sourceId); + const nodeIds = new Set(); + for (const edge of edges) { + nodeIds.add(edge.target); + } + return [...nodeIds] + .map((id) => this.nodes.get(id)) + .filter((n): n is ProvenanceNode => n !== undefined); + } + + toJSON(): object { + return { + nodes: Object.fromEntries(this.nodes), + edges: this.edges, + stats: { + nodeCount: this.nodes.size, + edgeCount: this.edges.length, + }, + }; + } + + static fromJSON(data: { + nodes: [string, ProvenanceNode][]; + edges: ProvenanceEdge[]; + }): ProvenanceGraphImpl { + const graph = new ProvenanceGraphImpl(); + for (const [, node] of data.nodes) { + graph.addNode(node); + } + for (const edge of data.edges) { + graph.addEdge(edge); + } + return graph; + } +} \ No newline at end of file diff --git a/reference-agent/src/sme.ts b/reference-agent/src/sme.ts new file mode 100644 index 0000000..ea44a05 --- /dev/null +++ b/reference-agent/src/sme.ts @@ -0,0 +1,76 @@ +/** + * SME (Subject Matter Expert) — Hyper-specialized single-task agent. + * + * SMEs are the leaf nodes of the Speckl agent hierarchy. + * Each SME does exactly one thing well: verify, generate, document, or integrate. + */ + +import type { + AgentId, + Task, + TaskMessage, + TaskResult, + TaskType, + ProvenanceEdge, + SpeckDefinition, +} from "./types.js"; +import { TillDoneTracker } from "./till-done.js"; +import { ProvenanceGraphImpl } from "./provenance.js"; + +export abstract class SME { + readonly id: AgentId; + protected provenance: ProvenanceGraphImpl; + protected tillDone: TillDoneTracker; + + constructor(name: string, specialization: string) { + this.id = { type: "sme", name, specialization }; + this.provenance = new ProvenanceGraphImpl(); + this.tillDone = new TillDoneTracker(); + } + + /** The task types this SME can handle. */ + abstract capabilities: TaskType[]; + + /** Can this SME handle the given task? */ + canHandle(task: Task): boolean { + return this.capabilities.includes(task.taskType); + } + + /** Execute a task and return the result. */ + abstract execute(task: Task, speck?: SpeckDefinition): Promise; + + /** Handle an incoming message from a Team Lead. */ + async handleMessage(message: TaskMessage): Promise { + if (message.type !== "task_assign") { + throw new Error(`SME ${this.id.name} cannot handle message type ${message.type}`); + } + + const task = message.payload.task; + const speck = message.payload.speck; + + // Register TillDone condition + this.tillDone.register(task.id, `Complete ${task.taskType} for ${task.speckName}`, (result) => + result.status === "success" + ); + + const result = await this.execute(task, speck); + + // Evaluate completion + this.tillDone.evaluate(task.id, result); + + // Record provenance + for (const edge of result.provenance) { + this.provenance.addEdge(edge); + } + + return { + id: `result-${task.id}-${Date.now()}`, + type: result.status === "success" ? "task_result" : "task_failed", + from: this.id, + to: message.from, + payload: { task, result }, + timestamp: new Date().toISOString(), + provenance: result.provenance, + }; + } +} \ No newline at end of file diff --git a/reference-agent/src/smes/codegen-sme.ts b/reference-agent/src/smes/codegen-sme.ts new file mode 100644 index 0000000..a93d964 --- /dev/null +++ b/reference-agent/src/smes/codegen-sme.ts @@ -0,0 +1,142 @@ +/** + * CodegenSME — Generates code from verified Specks. + * + * Takes a verified DST (Decision Structure Tree) and emits + * TypeScript or Rust code that provably satisfies the Speck. + */ + +import type { Task, TaskResult, SpeckDefinition, ProvenanceEdge } from "../types.js"; +import { SME } from "../sme.js"; + +export class CodegenSME extends SME { + readonly capabilities = ["generate_code"] as const; + + constructor(private targetLang: "typescript" | "rust" = "typescript") { + super(`codegen-${targetLang}`, "codegen"); + } + + async execute(task: Task, speck?: SpeckDefinition): Promise { + if (!speck) { + return { + taskId: task.id, + status: "failure", + provenance: [], + completedAt: new Date().toISOString(), + }; + } + + const code = this.generateCode(speck); + + const provenance: ProvenanceEdge[] = [ + { + source: `speck:${speck.name}`, + target: `code:${task.id}`, + relation: "generated_from", + tool: `speckl-codegen-${this.targetLang}`, + timestamp: new Date().toISOString(), + metadata: { + language: this.targetLang, + lineCount: code.split("\n").length, + }, + }, + ]; + + return { + taskId: task.id, + status: "success", + output: { + language: this.targetLang, + code, + speckName: speck.name, + }, + provenance, + completedAt: new Date().toISOString(), + }; + } + + /** Generate code from a Speck. Simplified for reference. */ + private generateCode(speck: SpeckDefinition): string { + if (this.targetLang === "typescript") { + return this.generateTypeScript(speck); + } + return this.generateRust(speck); + } + + private generateTypeScript(speck: SpeckDefinition): string { + const inputFields = Object.entries(speck.input) + .map(([name, type]) => { + const tsType = this.speckTypeToTS(type); + return ` ${name}: ${tsType};`; + }) + .join("\n"); + + const outputType = this.speckTypeToTS(speck.output); + + return `/** + * Generated from Speck: ${speck.name} + * Generated at: ${new Date().toISOString()} + * Constraints: ${speck.constraints.length} + * + * WARNING: This code was generated by the Speckl codegen SME. + * Do not edit directly. Modify the source Speck and regenerate. + */ + +export interface ${speck.name}Input { +${inputFields} +} + +export type ${speck.name}Output = ${outputType}; + +export function ${speck.name.toLowerCase()}(input: ${speck.name}Input): ${speck.name}Output { + // Constraint checks (runtime guards) +${speck.constraints.map((c) => ` // constraint: ${c.expression}`).join("\n")} +${speck.constraints.map((c) => ` // assert(${c.expression}, "${c.id}");`).join("\n")} + + // Implementation placeholder — in production, this would be + // compiled from the verified DST, not handwritten. + throw new Error("${speck.name}: implementation pending DST compilation"); +} +`; + } + + private generateRust(speck: SpeckDefinition): string { + return `// Generated from Speck: ${speck.name} +// Generated at: ${new Date().toISOString()} +// Constraints: ${speck.constraints.length} +// +// WARNING: This code was generated by the Speckl codegen SME. +// Do not edit directly. Modify the source Speck and regenerate. + +pub fn ${speck.name.toLowerCase()}() { + // Constraint checks +${speck.constraints.map((c) => ` // constraint: ${c.expression}`).join("\n")} + todo!("${speck.name}: implementation pending DST compilation"); +} +`; + } + + /** Map SpeckDL types to TypeScript types. */ + private speckTypeToTS(type: unknown): string { + if (typeof type === "string") { + const map: Record = { + Nat: "number", + Int: "number", + Real: "number", + Bool: "boolean", + String: "string", + Bytes: "Uint8Array", + }; + return map[type] ?? "unknown"; + } + if (typeof type === "object" && type !== null) { + const obj = type as Record; + if (obj.kind === "record") { + return "object"; // Simplified + } + if (obj.kind === "list") { + return `Array<${this.speckTypeToTS(obj.element)}>`; + } + } + return "unknown"; + } +} \ No newline at end of file diff --git a/reference-agent/src/smes/verification-sme.ts b/reference-agent/src/smes/verification-sme.ts new file mode 100644 index 0000000..f096a25 --- /dev/null +++ b/reference-agent/src/smes/verification-sme.ts @@ -0,0 +1,104 @@ +/** + * VerificationSME — Runs Z3 verification on a Speck. + * + * Compiles constraints to SMT-LIB2, invokes Z3, + * and reports SAT/UNSAT results with counterexamples. + */ + +import type { Task, TaskResult, SpeckDefinition, ProvenanceEdge } from "../types.js"; +import { SME } from "../sme.js"; + +export class VerificationSME extends SME { + readonly capabilities = ["verify_speck"] as const; + + constructor() { + super("z3-verifier", "verification"); + } + + async execute(task: Task, speck?: SpeckDefinition): Promise { + if (!speck) { + return { + taskId: task.id, + status: "failure", + provenance: [], + completedAt: new Date().toISOString(), + }; + } + + // Compile constraints to SMT-LIB2 + const z3Assertions = speck.constraints.map((c) => + this.compileConstraint(c.expression, speck) + ); + + // In production, this would invoke Z3 via subprocess or WASM. + // For the reference implementation, we simulate the result. + const z3Result = this.simulateZ3(speck, z3Assertions); + + // Compile verification conditions + const verifyResults = speck.verify.map((vc) => ({ + id: vc.id, + expression: vc.expression, + proven: this.checkVerifyCondition(vc.expression, speck), + })); + + const allVerified = verifyResults.every((v) => v.proven); + + // Record provenance + const provenance: ProvenanceEdge[] = [ + { + source: `speck:${speck.name}`, + target: `z3:${task.id}`, + relation: "verified_by", + tool: "Z3 4.12.5", + timestamp: new Date().toISOString(), + metadata: { + constraintCount: speck.constraints.length, + verifyCount: speck.verify.length, + allVerified, + }, + }, + ]; + + return { + taskId: task.id, + status: allVerified ? "success" : "failure", + output: { + z3Result, + verifiedConditions: verifyResults, + contradictionsFound: allVerified ? 0 : 1, + }, + provenance, + completedAt: new Date().toISOString(), + }; + } + + /** Compile a SpeckDL constraint expression to SMT-LIB2. */ + private compileConstraint(expression: string, _speck: SpeckDefinition): string { + // Simplified: in production, this would parse SpeckDL AST. + // For reference, we emit a comment and the expression as-is. + return `(assert ${expression})`; + } + + /** Simulate Z3 result. In production, invoke Z3 binary. */ + private simulateZ3( + speck: SpeckDefinition, + _assertions: string[] + ): string { + // A real implementation would: + // 1. Write all assertions + check-sat to a temp file + // 2. Invoke z3 binary + // 3. Parse SAT/UNSAT result and model + // For now, assume SAT if constraints look reasonable. + const hasNegativeConstraint = speck.constraints.some((c) => + c.expression.includes("== 0") && c.expression.includes("not") + ); + return hasNegativeConstraint ? "unsat" : "sat"; + } + + /** Check a verification condition. Simplified for reference. */ + private checkVerifyCondition(expression: string, _speck: SpeckDefinition): boolean { + // In production, negate the condition and check UNSAT. + // Simplified: assume always/implies conditions pass. + return !expression.includes("UNSAT"); + } +} \ No newline at end of file diff --git a/reference-agent/src/team-lead.ts b/reference-agent/src/team-lead.ts new file mode 100644 index 0000000..2538bb0 --- /dev/null +++ b/reference-agent/src/team-lead.ts @@ -0,0 +1,122 @@ +/** + * TeamLead — Manages a group of SMEs for a specific domain. + * + * Receives tasks from the Orchestrator, decomposes them, + * assigns to SMEs, and aggregates results. + */ + +import type { + AgentId, + Task, + TaskMessage, + TaskResult, + TaskType, + SpeckDefinition, + ProvenanceEdge, +} from "./types.js"; +import { SME } from "./sme.js"; +import { TillDoneTracker } from "./till-done.js"; +import { ProvenanceGraphImpl } from "./provenance.js"; + +export class TeamLead { + readonly id: AgentId; + private smes: SME[] = []; + protected provenance: ProvenanceGraphImpl; + protected tillDone: TillDoneTracker; + + constructor(name: string, specialization: string) { + this.id = { type: "team_lead", name, specialization }; + this.provenance = new ProvenanceGraphImpl(); + this.tillDone = new TillDoneTracker(); + } + + /** Register an SME under this team lead. */ + registerSME(sme: SME): void { + this.smes.push(sme); + } + + /** Get the task types this team can handle via its SMEs. */ + get capabilities(): TaskType[] { + return [...new Set(this.smes.flatMap((sme) => sme.capabilities))]; + } + + /** Can this team handle the given task? */ + canHandle(task: Task): boolean { + return this.smes.some((sme) => sme.canHandle(task)); + } + + /** Handle a task assignment from the Orchestrator. */ + async handleAssignment( + message: TaskMessage, + speck?: SpeckDefinition + ): Promise { + const task = message.payload.task; + + // Find the right SME + const sme = this.smes.find((s) => s.canHandle(task)); + if (!sme) { + return { + taskId: task.id, + status: "failure", + output: { error: `No SME available for task type ${task.taskType}` }, + provenance: [], + completedAt: new Date().toISOString(), + }; + } + + // Register TillDone condition + this.tillDone.register( + task.id, + `${sme.id.name} completes ${task.taskType}`, + (result) => result.status === "success" + ); + + // Execute + const result = await sme.execute(task, speck); + + // Evaluate completion + this.tillDone.evaluate(task.id, result); + + // Merge provenance + for (const edge of result.provenance) { + this.provenance.addEdge(edge); + } + + return result; + } + + /** Get all SMEs in this team. */ + getTeam(): SME[] { + return [...this.smes]; + } + + /** Check if this team is at capacity (queue depth > threshold). */ + isAtCapacity(threshold: number = 5): boolean { + return this.pendingCount() > threshold; + } + + /** Number of pending tasks (not yet done). */ + private pendingCount(): number { + return this.tillDone.pending().length; + } +} + +// ─── Pre-built Team Lead configurations ────────────────────── + +import { VerificationSME } from "./smes/verification-sme.js"; +import { CodegenSME } from "./smes/codegen-sme.js"; + +export class VerificationTeamLead extends TeamLead { + constructor() { + super("verification-lead", "verification"); + this.registerSME(new VerificationSME()); + } +} + +export class CodegenTeamLead extends TeamLead { + constructor() { + super("codegen-lead", "codegen"); + this.registerSME(new CodegenSME("typescript")); + this.registerSME(new CodegenSME("rust")); + } +} \ No newline at end of file diff --git a/reference-agent/src/till-done.ts b/reference-agent/src/till-done.ts new file mode 100644 index 0000000..020dd0a --- /dev/null +++ b/reference-agent/src/till-done.ts @@ -0,0 +1,73 @@ +/** + * TillDone — Condition-based task tracking for Speckl. + * + * Tasks don't tick boxes. They evaluate predicates. + * "Done" means a proven condition is met. + */ + +import type { TillDoneCondition, TaskResult } from "./types.js"; + +export class TillDoneTracker { + private conditions: Map = new Map(); + + /** Register a completion condition for a task. */ + register(taskId: string, description: string, predicate: (result: TaskResult) => boolean): void { + this.conditions.set(taskId, { + taskId, + description, + predicate, + isDone: false, + }); + } + + /** Evaluate a task result against its condition. */ + evaluate(taskId: string, result: TaskResult): boolean { + const condition = this.conditions.get(taskId); + if (!condition) { + throw new Error(`No TillDone condition registered for task ${taskId}`); + } + + const satisfied = condition.predicate(result); + condition.isDone = satisfied; + return satisfied; + } + + /** Check if a task's condition has been met. */ + isDone(taskId: string): boolean { + return this.conditions.get(taskId)?.isDone ?? false; + } + + /** Get all pending (not done) conditions. */ + pending(): TillDoneCondition[] { + return [...this.conditions.values()].filter((c) => !c.isDone); + } + + /** Get all completed conditions. */ + completed(): TillDoneCondition[] { + return [...this.conditions.values()].filter((c) => c.isDone); + } + + /** Built-in predicates for common Speckl conditions. */ + static predicates = { + /** Z3 verification returned SAT (constraints satisfiable). */ + z3Verified: (result: TaskResult): boolean => + result.status === "success" && + (result.output as Record)?.z3Result === "sat", + + /** All constraints are satisfiable (no contradictions). */ + noContradictions: (result: TaskResult): boolean => + result.status === "success" && + (result.output as Record)?.contradictions === 0, + + /** Code generation produced valid output. */ + codeGenerated: (result: TaskResult): boolean => + result.status === "success" && + typeof (result.output as Record)?.code === "string", + + /** Provenance graph is complete for this Speck. */ + provenanceComplete: (result: TaskResult): boolean => + result.status === "success" && + Array.isArray(result.provenance) && + result.provenance.length > 0, + }; +} \ No newline at end of file diff --git a/reference-agent/src/types.ts b/reference-agent/src/types.ts new file mode 100644 index 0000000..7c09802 --- /dev/null +++ b/reference-agent/src/types.ts @@ -0,0 +1,157 @@ +/** + * Speckl Reference Agent Architecture + * + * Core types and protocols for the tiered agent harness. + * Orchestrator → Team Lead → SME hierarchy with TillDone condition tracking. + */ + +// ─── Speck Types ──────────────────────────────────────────── + +export interface SpeckDefinition { + name: string; + input: Record; + output: SpeckType; + constraints: Constraint[]; + verify: VerifyCondition[]; + events?: EventDef[]; + imports?: ImportRef[]; + interface?: string; +} + +export type SpeckType = + | PrimitiveType + | RecordType + | ListType + | NamedType; + +export type PrimitiveType = "Nat" | "Int" | "Real" | "Bool" | "String" | "Bytes"; + +export interface RecordType { + kind: "record"; + fields: Record; +} + +export interface ListType { + kind: "list"; + element: SpeckType; +} + +export interface NamedType { + kind: "named"; + name: string; + typeArgs?: SpeckType[]; +} + +export interface Constraint { + id: string; + expression: string; // SpeckDL expression text + compiledToZ3?: string; // SMT-LIB2 assertion +} + +export interface VerifyCondition { + id: string; + kind: "always" | "eventually" | "implies"; + expression: string; + proven?: boolean; + counterexample?: Record; +} + +export interface EventDef { + name: string; + fields: Record; +} + +export interface ImportRef { + path: string; + alias?: string; +} + +// ─── Agent Protocol ───────────────────────────────────────── + +export type TaskStatus = "pending" | "in_progress" | "blocked" | "completed" | "failed"; + +export interface TaskMessage { + id: string; + type: "task_assign" | "task_result" | "task_blocked" | "task_failed"; + from: AgentId; + to: AgentId; + payload: TaskPayload; + timestamp: string; // ISO 8601 + provenance: ProvenanceEdge[]; +} + +export interface TaskPayload { + task: Task; + speck?: SpeckDefinition; + context?: Record; +} + +export interface Task { + id: string; + speckName: string; + taskType: TaskType; + description: string; + priority: number; + parentTaskId?: string; + createdAt: string; +} + +export type TaskType = + | "verify_speck" // Run Z3 verification on a Speck + | "compile_to_dst" // Compile verified Speck to DST + | "compile_to_wasm" // Compile DST to WASM + | "generate_code" // Generate code from verified Speck + | "generate_docs" // Generate documentation from provenance graph + | "integrate" // Integration/glue code + | "review" // Human review checkpoint + ; + +export interface AgentId { + type: "orchestrator" | "team_lead" | "sme"; + name: string; + specialization?: string; +} + +export interface ProvenanceEdge { + source: string; // URI or ID of the source artifact + target: string; // URI or ID of the derived artifact + relation: string; // "compiled_to" | "verified_by" | "generated_from" | "derived_from" + tool: string; // Tool that created this edge + timestamp: string; + metadata?: Record; +} + +// ─── TillDone Condition Tracking ───────────────────────────── + +export interface TillDoneCondition { + taskId: string; + description: string; + predicate: (result: TaskResult) => boolean; + isDone: boolean; +} + +export interface TaskResult { + taskId: string; + status: "success" | "failure"; + output?: unknown; + provenance: ProvenanceEdge[]; + completedAt: string; +} + +// ─── Provenance Graph ─────────────────────────────────────── + +export interface ProvenanceNode { + id: string; + type: "speck" | "z3_assertion" | "dst" | "wasm" | "code" | "docs" | "event"; + label: string; + metadata: Record; +} + +export interface ProvenanceGraph { + nodes: Map; + edges: ProvenanceEdge[]; + addNode(node: ProvenanceNode): void; + addEdge(edge: ProvenanceEdge): void; + query(source?: string, relation?: string, target?: string): ProvenanceEdge[]; + toJSON(): object; +} \ No newline at end of file diff --git a/reference-agent/tsconfig.json b/reference-agent/tsconfig.json new file mode 100644 index 0000000..deeaa2e --- /dev/null +++ b/reference-agent/tsconfig.json @@ -0,0 +1,24 @@ +{ + "compilerOptions": { + "target": "ES2022", + "module": "ESNext", + "moduleResolution": "bundler", + "outDir": "dist", + "rootDir": "src", + "declaration": true, + "declarationMap": true, + "sourceMap": true, + "strict": true, + "noUnusedLocals": true, + "noUnusedParameters": true, + "noFallthroughCasesInSwitch": true, + "exactOptionalPropertyTypes": true, + "esModuleInterop": true, + "skipLibCheck": true, + "forceConsistentCasingInFileNames": true, + "resolveJsonModule": true, + "declarationDir": "dist/types" + }, + "include": ["src/**/*.ts"], + "exclude": ["node_modules", "dist"] +} diff --git a/speckdl/SPEC.md b/speckdl/SPEC.md new file mode 100644 index 0000000..d26718a --- /dev/null +++ b/speckdl/SPEC.md @@ -0,0 +1,389 @@ +# SpeckDL Language Specification v0.1 + +> The specification-first language for auditable software. +> Part of the [Speckl](https://os.scoble.me/forgejo/sscoble/speckl) project. MIT License. + +--- + +## 1. Introduction + +SpeckDL is a domain-specific language for defining system behavior and interfaces. A SpeckDL specification (a **Speck**) describes *what* a system should do, not *how* it should do it. Specks compile through a deterministic pipeline — SpeckDL → Z3 → DST → WASM — producing verified artifacts with full dark provenance. + +### Design Goals + +- **Human-readable first.** A Speck should be understandable by a domain expert who doesn't write code. +- **Machine-verifiable.** Every constraint in a Speck compiles to Z3 (SMT solver) input. Verification is automatic. +- **Provenance-native.** The compilation pipeline records derivation edges automatically. Provenance is not bolted on — it's structural. +- **Composable.** Specks compose via interfaces. Large systems are built from small, verified Specks. +- **Deterministic.** Same input, same output. No LLMs in the compilation path. + +--- + +## 2. Syntax + +### 2.1 Top-Level Structure + +A SpeckDL file consists of one or more Speck definitions: + +``` +speck { + +} +``` + +Members are drawn from: `input`, `output`, `constraint`, `verify`, `interface`, `import`, and `event`. + +### 2.2 EBNF Grammar + +```ebnf +file = { speck_def | import_stmt } + +speck_def = "speck" IDENT "{" { member } "}" + +member = input_def | output_def | constraint_def + | verify_def | interface_def | event_def + +input_def = "input" ":" type_expr +output_def = "output" ":" type_expr + +type_expr = primitive | compound | IDENT +primitive = "Nat" | "Int" | "Real" | "Bool" | "String" | "Bytes" +compound = "{" { IDENT ":" type_expr [","] } "}" + | "[" type_expr "]" + +constraint_def = "constraint" ":" expr +verify_def = "verify" ":" temporal_expr + +expr = literal | IDENT | expr op expr | expr "." IDENT + | func_call | "(" expr ")" +op = "==" | "!=" | "<=" | ">=" | "<" | ">" + | "+" | "-" | "*" | "/" | "mod" + | "and" | "or" | "not" | "implies" +func_call = IDENT "(" [expr { "," expr }] ")" + +temporal_expr = "always" "(" expr ")" + | "eventually" "(" expr ")" + | "implies" "(" expr "," expr ")" + +interface_def = "interface" IDENT "{" { method_sig } "}" +method_sig = IDENT "(" [ { IDENT ":" type_expr "," } ] ")" ":" type_expr + +event_def = "event" IDENT "{" { IDENT ":" type_expr [","] } "}" + +import_stmt = "import" STRING ["as" IDENT] + +literal = NAT_LIT | INT_LIT | REAL_LIT | BOOL_LIT | STRING_LIT +IDENT = letter { letter | digit | "_" } +``` + +### 2.3 Type System + +| Type | Meaning | Z3 Mapping | +|------|---------|------------| +| `Nat` | Non-negative integer | `Int` with constraint `>= 0` | +| `Int` | Signed integer | `Int` | +| `Real` | Real number | `Real` | +| `Bool` | Boolean | `Bool` | +| `String` | UTF-8 string | Uninterpreted sort | +| `Bytes` | Byte sequence | Uninterpreted sort | +| `{ ... }` | Record/tuple | Datatype | +| `[T]` | List of T | Seq(T) | + +--- + +## 3. Semantics + +### 3.1 Speck Definitions + +A Speck defines a behavioral unit with: +- **Inputs:** Typed parameters the Speck accepts. +- **Outputs:** Typed results the Speck produces. +- **Constraints:** Invariants that must hold for all valid inputs and outputs. +- **Verification conditions:** Temporal properties that the Z3 solver must prove. + +A Speck is *well-formed* if: +1. All referenced identifiers are in scope. +2. No two constraints are contradictory (Z3 must report SAT for the conjunction of all constraints). +3. All verification conditions are provable from the constraints. + +### 3.2 Constraint Semantics + +A `constraint` defines an invariant that must hold across all valid executions of the Speck. Constraints are compiled to Z3 assertions: + +``` +constraint: maxRetries <= 5 +``` + +becomes: + +```smt2 +(assert (<= maxRetries 5)) +``` + +Constraints are **universally quantified** over all inputs unless explicitly scoped. + +### 3.3 Verification Semantics + +A `verify` clause defines a property that must be provable from the Speck's constraints: + +``` +verify: always(implies(attempt > 1, delay > 0)) +``` + +becomes: + +```smt2 +(assert (=> (> attempt 1) (> delay 0))) +(check-sat) +``` + +If Z3 returns `UNSAT` when asked to negate a verification condition, the condition is proven. If Z3 returns `SAT`, the Speck contains a counterexample — it can be violated. + +### 3.4 Interface Semantics + +An interface defines a contract between Specks. A Speck that provides an interface must satisfy all constraints of that interface: + +``` +interface PaymentProcessor { + charge(amount: Real, currency: String): Result + refund(transactionId: Nat): Result +} + +speck StripeProcessor { + interface: PaymentProcessor + input: { apiKey: String } + output: Result + constraint: amount > 0 + constraint: currency in ["USD", "EUR", "GBP"] +} +``` + +### 3.5 Event Semantics + +Events define state transitions that the provenance graph records: + +``` +event RetryAttempted { + attemptNumber: Nat + delay: Real + remainingRetries: Nat +} +``` + +Events are emitted during execution and recorded as nodes in the provenance graph. They do not affect the verification pipeline — they exist for observability. + +--- + +## 4. Compilation Pipeline + +### 4.1 Stage 1: SpeckDL → Z3 + +Each Speck is compiled to SMT-LIB2 format: + +1. Type declarations become Z3 sort declarations. +2. Input/output declarations become Z3 constants. +3. Constraints become `assert` statements. +4. Verification conditions become `check-sat` queries. + +The compiler checks for: +- **Contradictory constraints:** If the conjunction of all constraints is UNSAT, the Speck is impossible to implement. +- **Unsatisfiable verification conditions:** If a verify clause can be violated, the compiler reports the counterexample. + +### 4.2 Stage 2: Z3 → DST (Decision Structures) + +When Z3 reports SAT for a Speck, the model (assignment of values satisfying all constraints) is compiled into a **Decision Structure Tree**: + +``` +DSTNode { + condition: expr // branching predicate + if_true: DSTNode // subtree when condition holds + if_false: DSTNode // subtree when condition doesn't hold + result: value? // leaf value (if terminal) +} +``` + +A DST represents the complete behavioral space of a verified Speck. Every possible input maps to exactly one path through the DST, terminating at a leaf with the verified output. + +### 4.3 Stage 3: DST → WASM + +DSTs compile to WebAssembly via a direct translation: + +- Each DST node becomes a `br_if` / `br` instruction pair. +- Leaf values become `i32.const`, `f64.const`, or structured return values. +- The resulting WASM module exports a single function matching the Speck's input/output signature. + +This compilation is *semantics-preserving by construction*: the WASM module implements exactly the behaviors encoded in the DST, which represents exactly the satisfiable space of the Speck. + +### 4.4 Provenance Graph Construction + +At each compilation stage, the pipeline records derivation edges: + +``` +Speck "RetryHandler" + ├── compiled_to → Z3 assertion set (sha256:abc...) + ├── verified_by → Z3 result: SAT + ├── compiled_to → DST (sha256:def...) + ├── compiled_to → WASM module (sha256:789...) + └── provenance: { + author: "scott", + timestamp: "2026-04-28T09:00:00Z", + tool: "speckl-compiler v0.1", + z3_version: "4.12.5" + } +``` + +The provenance graph is serialized as JSON-LD and stored alongside the compiled artifacts. + +--- + +## 5. Examples + +### 5.1 Simple: API Rate Limiter + +``` +speck RateLimiter { + input: { requests: [Request], window: Nat, maxRequests: Nat } + output: { allowed: [Bool], remaining: Nat } + constraint: maxRequests > 0 + constraint: window > 0 + constraint: count(allowed, true) <= maxRequests + constraint: remaining == maxRequests - count(allowed, true) + verify: always(implies(remaining == 0, not(allowed[current]))) +} +``` + +### 5.2 Medium: Data Pipeline with Constraints + +``` +speck ETLTransform { + input: { source: DataSource, schema: Schema, dedup: Bool } + output: { result: Dataset, rejected: Nat } + constraint: result.schema == schema + constraint: rejected >= 0 + constraint: implies(dedup, count(result) <= count(source)) + constraint: implies(not dedup, count(result) == count(source)) + verify: always(implies(dedup, no_duplicates(result))) +} +``` + +### 5.3 Complex: Regulated Medical Device Function + +``` +speck DrugDosageCalculator { + input: { + patientWeight: Real, + drugConcentration: Real, + prescribedDose: Real, + minDose: Real, + maxDose: Real, + frequency: Nat + } + output: { + volume: Real, + safe: Bool + } + constraint: patientWeight > 0 + constraint: drugConcentration > 0 + constraint: minDose > 0 + constraint: maxDose > minDose + constraint: frequency >= 1 + constraint: frequency <= 6 + constraint: implies(safe, volume >= minDose / drugConcentration) + constraint: implies(safe, volume <= maxDose / drugConcentration) + constraint: implies(not safe, volume == 0) + verify: always(implies( + prescribedDose >= minDose and prescribedDose <= maxDose, + safe + )) + verify: always(implies(not safe, volume == 0)) + event DoseCalculated { volume: Real, safe: Bool } + event DoseRejected { reason: String } +} +``` + +### 5.4 Edge: Self-Referential Spec + +``` +speck SpeckValidator { + input: { spec: SpeckDefinition, references: [SpeckDefinition] } + output: { valid: Bool, errors: [String] } + constraint: implies(valid, count(errors) == 0) + constraint: implies(not valid, count(errors) > 0) + constraint: forall(ref in references, ref.is_well_formed) + verify: always(implies( + spec.is_well_formed and forall(r in references, r.is_well_formed), + valid + )) +} +``` + +### 5.5 Composed: Multi-Speck System + +``` +speck PaymentService { + import "rate-limiter.speck" as limiter + import "retry-handler.speck" as retry + + input: { payment: Payment, apiKey: String } + output: Result + + constraint: limiter.maxRequests == 100 + constraint: limiter.window == 60 + constraint: retry.maxRetries == 3 + constraint: implies(not limiter.allowed, output == RateLimited) + constraint: implies(limiter.allowed, output in [Success, Failed, RetryExhausted]) + + verify: always(implies( + limiter.remaining == 0, + output == RateLimited + )) +} +``` + +--- + +## 6. Tooling + +### Reference Compiler + +The reference compiler (`speckl-compile`) is a Node.js/TypeScript application that: + +1. Parses SpeckDL files into an AST. +2. Type-checks the AST against the type system defined in §3. +3. Compiles constraints and verification conditions to SMT-LIB2. +4. Invokes Z3 and interprets results. +5. Compiles verified models to DSTs. +6. Compiles DSTs to WASM. +7. Emits provenance graph metadata (JSON-LD) at each stage. + +### Planned Tooling + +| Tool | Purpose | Status | +|------|---------|--------| +| `speckl-compile` | Reference compiler | Spec only | +| `speckl-lsp` | Language Server Protocol (IDE support) | Planned | +| `speckl-playground` | Browser-based spec editor + live verification | Planned | +| `speckl-fmt` | Formatter | Planned | +| `speckl-doc` | Documentation generator from Specks | Planned | + +--- + +## Appendix A: Z3 Mapping Reference + +| SpeckDL Construct | SMT-LIB2 | +|---|---| +| `Nat n` | `(declare-const n Int)` + `(assert (>= n 0))` | +| `Int n` | `(declare-const n Int)` | +| `Real r` | `(declare-const r Real)` | +| `Bool b` | `(declare-const b Bool)` | +| `constraint: e` | `(assert e)` | +| `verify: always(e)` | `(assert (not e))` + `(check-sat)` — expect UNSAT | +| `verify: eventually(e)` | Not directly expressible; requires bounded model checking | +| `a == b` | `(= a b)` | +| `a implies b` | `(=> a b)` | +| `a and b` | `(and a b)` | +| `forall(x in S, e)` | `(forall ((x T)) (=> (member x S) e))` | + +--- + +*This is a v0.1 specification. The language is evolving. Feedback and contributions are welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).* \ No newline at end of file