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

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

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": {}
+}

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<string, SpeckDefinition> = {
+  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<void> {
+  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 <name>    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);
+});

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<OrchestrationResult> {
+    const startTime = Date.now();
+    const results: Map<string, TaskResult> = 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<string, TaskResult>
+  ): 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<string, TaskResult>;
+  provenance: object;
+  durationMs: number;
+  error?: string;
+}

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<string, ProvenanceNode> = 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<string>();
+    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<string>();
+    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;
+  }
+}

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<TaskResult>;
+
+  /** Handle an incoming message from a Team Lead. */
+  async handleMessage(message: TaskMessage): Promise<TaskMessage> {
+    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,
+    };
+  }
+}

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<TaskResult> {
+    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<string, string> = {
+        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<string, unknown>;
+      if (obj.kind === "record") {
+        return "object"; // Simplified
+      }
+      if (obj.kind === "list") {
+        return `Array<${this.speckTypeToTS(obj.element)}>`;
+      }
+    }
+    return "unknown";
+  }
+}

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<TaskResult> {
+    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");
+  }
+}

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<TaskResult> {
+    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"));
+  }
+}

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<string, TillDoneCondition> = 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<string, unknown>)?.z3Result === "sat",
+
+    /** All constraints are satisfiable (no contradictions). */
+    noContradictions: (result: TaskResult): boolean =>
+      result.status === "success" &&
+      (result.output as Record<string, unknown>)?.contradictions === 0,
+
+    /** Code generation produced valid output. */
+    codeGenerated: (result: TaskResult): boolean =>
+      result.status === "success" &&
+      typeof (result.output as Record<string, unknown>)?.code === "string",
+
+    /** Provenance graph is complete for this Speck. */
+    provenanceComplete: (result: TaskResult): boolean =>
+      result.status === "success" &&
+      Array.isArray(result.provenance) &&
+      result.provenance.length > 0,
+  };
+}

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<string, SpeckType>;
+  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<string, SpeckType>;
+}
+
+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<string, unknown>;
+}
+
+export interface EventDef {
+  name: string;
+  fields: Record<string, SpeckType>;
+}
+
+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<string, unknown>;
+}
+
+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<string, unknown>;
+}
+
+// ─── 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<string, unknown>;
+}
+
+export interface ProvenanceGraph {
+  nodes: Map<string, ProvenanceNode>;
+  edges: ProvenanceEdge[];
+  addNode(node: ProvenanceNode): void;
+  addEdge(edge: ProvenanceEdge): void;
+  query(source?: string, relation?: string, target?: string): ProvenanceEdge[];
+  toJSON(): object;
+}

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"]
+}