Design Pillars

• Readable and writable by every Markdown editor — Spec files are plain Markdown with standard fenced blocks and blockquote directives. Any editor that supports frontmatter works without plugins.
• Understandable by all stakeholders — Prose, tables, and results are readable by designers, PMs, and QA — not just engineers. The document is the spec, not a wrapper around code.
• Adapters are ordinary processes — Any language works. An adapter is just an executable that reads and writes NDJSON on stdin/stdout. No SDK, no plugin API, no runtime coupling.
• Core knows nothing about products — The core parses Markdown and routes cases. It never imports test frameworks, knows filesystem layouts, or interprets block semantics. All domain logic lives in adapters.

Architecture

Two pipelines diverge from a single document.

Spec Document (.spec.md)
    |
    +-- Core
    |     +-- heading / prose / block / table parsing
    |     +-- variable scope computation
    |     +-- executable unit ID assignment
    |     +-- embedded Alloy model extraction
    |
    +-- Runtime Adapter
    |     +-- test execution + event emission
    |
    +-- Reporter
    |     +-- HTML / JSON artifact generation
    |
    +-- Alloy Runner
          +-- model check + event emission

The core parses the document and produces an execution plan — a list of blocks and table rows tagged with adapter names. It never executes anything itself. The runtime adapter receives each unit, runs the actual code, and emits pass/fail events. The reporter collects those events and renders the final HTML or JSON output. The Alloy runner is a parallel path: it extracts embedded model fragments, invokes the Alloy solver, and feeds results into the same event stream.

All four components communicate through a common event schema. This means a new reporter or a new adapter can be added without changing the core.

Core and Adapter Boundary

Core parses spec documentsdepends and produces an execution plan. Adapters execute it via the adapter protocoldepends.

Core is responsible for:

• Markdown parsing and heading hierarchy
• Extracting code blocks, directives, and tables
• Variable binding and scope computation
• SpecID generation
• Combining embedded Alloy fragments
• Generating a runtime-independent execution plan
• Defining the common event schema

Adapters are responsible for:

• Interpreting block semantics (run:*, doctest-style)
• Interpreting column semantics of check tables
• Connecting to external execution environments

Reporters are responsible for:

• Rendering execution results as HTML/JSON from the event stream

Core must not know about any specific test framework, product-specific filesystem layouts, product-specific command vocabularies, or the adapter implementation language.

A dry run demonstrates the boundary: the core parses and validates without launching any adapter.

Event Schema

All components communicate through a common event type. Each event carries a type, a case identifier, and optional diagnostic fields:

Events flow from adapters and the Alloy runner into case results. The reporter never sees raw adapter protocol messages — only the unified event stream assembled by the engine.

Reporter Contract

A reporter receives a Report value after execution completes and writes output artifacts. The report contains:

• Title — derived from the entry document heading.
• Results — one DocumentResult per spec, each holding an ordered list of CaseResult values.
• Summary — aggregate counts: specs total/passed/failed, cases total/passed/failed/expected-fail.
• TraceErrors — validation messages from the traceability checker (if configured).
• TraceGraph — the document graph with typed edges (if configured).

Two built-in reporters are supported:

• html — writes a multi-page HTML site with a global table of contents, per-document pages, shared CSS/JS assets, and optional trace graph visualization.
• json — writes the full Report struct as indented JSON.

Reporter selection is configured in specdown.jsondepends via the reporters array. Each entry specifies a builtin name and an outFile path.

The JSON report is machine-readable and can be verified:

Parallel Execution

When -jobs N is greater than 1, the engine executes documents concurrently using a semaphore of size N. Each document gets its own adapter sessions — sessions are never shared across documents.

Within a single document, cases execute sequentially in document order. Variable bindings from earlier blocks are available to later blocks within the same scope.

The default is -jobs 1 (sequential). Setting -jobs to the number of CPU cores is safe because each goroutine blocks on adapter I/O, not CPU.

Sequential execution is the default:

Alloy Runner Integration

The Alloy runner implements the ModelRunner interface:

ModelRunner
  RunDocument(plan) -> []CaseResult

For each document, the runner:

1. Collects all CaseKindAlloy cases from the plan.
2. Groups them by model name.
3. Bundles embedded Alloy fragments into a single .als file per model.
4. Invokes the Alloy solver (Java subprocess) on each bundle.
5. Maps solver output back to individual assertion results.

The runner caches the Alloy JAR in ~/.cache/specdown/. If the JAR is missing, it downloads the official release automatically.

Alloy cases run in parallel with adapter cases at the document level and their results are merged into the same DocumentResult.