Internals
This chapter describes how specdown is built. It is not required for writing specs, but helps adapter authors and contributors understand the core/adapter/reporter separation.
You can verify the tool is available and see its version:
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
Four components process a spec document:
- Core — parses Markdown (headings, prose, blocks, tables), computes variable scopes, assigns executable unit IDs, and extracts embedded Alloy model fragments. Produces an execution plan — a list of blocks and table rows tagged with adapter names. Never executes anything itself.
- ModelRunner — the engine calls
ModelRunner.RunDocument()before the case loop. Model verification results are pre-indexed and looked up inline during case processing, flowing through the same case sequence as adapter results. - Runtime Adapter — receives each unit, runs the actual code, and emits pass/fail events.
- Reporter — collects events and renders the final HTML or JSON output.
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
SpecIDgeneration- 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.
... (1 line)
Event Schema
All components communicate through a common event type. Each event carries a type, a case identifier, and optional diagnostic fields:
| Field | Type | Description |
|---|---|---|
| type | string | caseStarted, casePassed, or caseFailed |
| id | SpecID | Unique identifier for the case |
| label | string | Human-readable description of the case |
| message | string | Failure reason (failed events only) |
| expected | string | Expected value (failed events only) |
| actual | string | Actual value (failed events only) |
| bindings | array | Variable bindings captured during execution |
Events flow from adapters into case results; model verification
results (via ModelRunner) are pre-computed and looked up inline.
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
DocumentResultper spec, each holding an ordered list ofCaseResultvalues. Kind-specific fields are nested incode,table, oralloysub-structs. - 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
Reportstruct as indented JSON. The report includes aschemaVersionfield (currently2).
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:
Create a minimal project and run it with a JSON reporter
mkdir -p reporter-json/specs
printf '# T\n\n- [S](s.spec.md)\n' > reporter-json/specs/index.spec.md
printf '# S\n\nProse.\n' > reporter-json/specs/s.spec.md
cat <<'CFG' > reporter-json/specdown.json
{"entry":"specs/index.spec.md","adapters":[],"reporters":[{"builtin":"json","outFile":"out.json"}]}
CFG
specdown run -config reporter-json/specdown.json -quiet 2>&1 | tail -1Parallel 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:
... (1 line)
Alloy Runner Integration
The engine calls ModelRunner.RunDocument() before the case loop.
Results are indexed by SpecID and looked up inline during case
processing. The ModelRunner interface keeps model verification
decoupled from the engine.
ModelRunner
RunDocument(plan) -> []CaseResult
For each document, the runner:
- Collects all
CaseKindAlloycases from the plan. - Groups them by model name.
- Bundles embedded Alloy fragments into a single
.alsfile per model. - Invokes the Alloy solver (Java subprocess) on each bundle.
- 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.
Model results are pre-computed via ModelRunner before the case loop;
alloy cases execute in document order within the normal case sequence.
Alloy failures respect -max-failures and stream progress inline.