# 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