Generated banner for Spec To Code Compliance
Generated logo for Spec To Code Compliance

Spec To Code Compliance

Trail of BitsOfficialPublished by Trail of Bits

  • Skill
  • Review and audit
  • Software development
  • CC-BY-SA-4.0
  • Medium risk

From the author

Check code against the documentation that specifies it - which requirements hold, which the code contradicts, which are absent, and what the code does that no document mentions. Use when comparing an implementation against a whitepaper, protocol spec, or design document.
— the description by Trail of Bits

AutoGineer summary

Written by AutoGineer from the skill’s own files, not by the author

Spec-to-Code Compliance is a specialized workflow designed to identify discrepancies between authoritative documentation and actual code implementation. By decomposing specifications into individual requirements, it deploys independent agents to verify each against the codebase. The process includes a rigorous refutation phase where separate agents attempt to disprove findings, ensuring that reported divergences are genuine. The output provides a structured report detailing the status of each requirement, including verdicts like implemented, partial, contradicted, or absent, along with evidence records for each finding.

What it does

  • Parses documentation to extract individually checkable requirements.
  • Dispatches independent agents to verify code compliance against specific requirements.
  • Performs a refutation pass to validate findings and reduce false positives.
  • Generates a comprehensive compliance report with per-requirement analysis.
  • Identifies undocumented code behavior not mentioned in the specification.
  • Provides evidence-based records for each verdict, including search patterns and code paths.

When to use it

  • When verifying that a codebase adheres to an authoritative specification, whitepaper, or protocol.
  • When auditing services or contracts against design documentation.
  • When you need to identify gaps between stated guarantees in a README and the actual implementation.
  • When you require a verifiable audit trail of compliance checks for security or quality assurance.

Advantages

  • Reduces context window limitations by checking requirements individually.
  • Minimizes false positives through a multi-agent refutation process.
  • Provides granular evidence for each finding, including specific code lines and search results.
  • Distinguishes between documentation drift and actual implementation defects.

Usage examples

“Run spec-compliance on ./src against DESIGN.md, checking 15 requirements.”
The agent parses DESIGN.md, splits it into 15 requirements, and runs individual verification agents for each, producing a report in spec-compliance/REPORT.md.
“Run spec-compliance on ./contracts against PROTOCOL.md.”
The agent analyzes the contract code against the protocol specification and identifies any contradictions, absent requirements, or undocumented behaviors.

Install

  1. Download the skill as a ZIP:

    https://autogineer.com/agent-skills/trailofbits/spec-to-code-compliance/download
  2. Unzip it into the cross-client skills folder of your project:

    mkdir -p .agents/skills && unzip spec-to-code-compliance.zip -d .agents/skills

Documentation by Trail of Bits

Spec-to-Code Compliance

Two artifacts disagree, and the job is to find where. The documentation says what the system does; the code decides what it actually does. Every gap between them is either a bug or a documentation fix, and which one it is is the finding.

When to Use

You have both documentation describing intended behavior and the code that should implement it. A whitepaper against a protocol, a design note against a service, a README's stated guarantees against the functions behind them.

Most useful when the document is authoritative — something a client wrote, published, or is audited against — because then a divergence is a defect rather than stale prose.

When NOT to Use

Not for code with no documentation of intended behavior. There is nothing to check against, and a requirement inferred from the code is checked against itself. Build the system model first with audit-context-building.

Not for finding bugs in general. This finds one class: where the code and the document disagree. A bug both artifacts are silent about is out of scope, and a bug the document endorses is a finding against the document.

Not for writing or improving documentation, though it produces the list of what needs fixing.

Do not check requirements in this context

Run /spec-to-code-compliance:spec-compliance <path>. The slash command takes a path; to name the specification directly or widen the fan-out, ask for the run with those values — "run spec-compliance on ./contracts against SPEC.md, checking 20 requirements" — and they reach the script as {path, spec, limit}. Typing the object literally after the slash command does not work; it arrives as a string and becomes the path.

It finds the documents, splits them into individually checkable requirements, gives each requirement its own agent to hunt the code with, has independent agents try to refute every divergence before it is reported, and writes spec-compliance/REPORT.md plus one file per requirement under spec-compliance/requirements/. Only compact records come back here.

For a single requirement, dispatch the spec-to-code-compliance:spec-compliance-checker agent at it.

This is not a preference about where output lands. The check does not fit in one context window if it is done honestly: judging one requirement means reading the enforcement, its callees, and its callers, and doing that for thirty requirements means holding thirty call chains at once. Attempted inline, the first few get a real check and the rest get a plausible one — and the transcript looks the same either way, because a verdict resting on a promising function name reads exactly like one resting on having read the function. Per requirement, in its own context, is what makes that difference visible.

Two properties come from the script rather than from instructions, and cannot be had here:

  • A refutation the finding's author did not perform. Claude favors findings it produced when asked to check them. The workflow sends each divergence to agents that did not produce it — one reading the code again, one re-reading the document — and drops what either knocks down.

  • Records that cannot be prose. A subagent bound to a return schema has to name the lines it read and the searches it ran. An absent verdict arrives with the patterns tried and their results attached, which is the only thing separating a real absence from a search that stopped early.

Measured on the routes-not-inline eval: with this plugin installed the work is dispatched every run, without it never — Δ +1.00. Deleting this section while leaving the workflow in place changes nothing, because the workflow is a real command that gets found and dispatched on its own. Read that as the mechanism carrying the behavior rather than this text: the section is here so a human knows what runs and why, not because the routing depends on it.

What comes back, and how to read it

Every requirement gets one of six verdicts: implemented, partial, contradicted, stronger-than-spec, absent, or undecidable. The interesting ones are the middle four.

  • partial is usually the most serious thing in the report. The requirement holds on the paths anyone would test and fails on one nobody did, which is how it survived long enough to be found.

  • absent rests entirely on its searched record. Read it. Enforcement often lives somewhere the search did not go — a modifier, a base class, a caller that checks first.

  • undecidable, and any documentProblem, are findings about the documentation. A requirement too vague to check is one the client cannot hold anyone to.

  • stronger-than-spec is an undocumented constraint. It works today, and nothing tells the next person changing that code that anything depended on it.

The report also carries the reverse direction — behavior the code has that no document mentions — which the per-requirement pass cannot find by construction, since it is driven by the documents.

Read notChecked, unverified, and unreadableDocuments before treating the report as complete. Requirements below the fan-out cut were never checked, and a divergence whose refutation agents both failed is unverified rather than confirmed.

Judgment the workflow does not make for you

Severity is consequence, not distance from the text: DIVERGENCE_RUBRIC.md. A rounding step that bleeds a pool outranks a MUST satisfied by different means than the document describes, and documentation drift with no behavioral consequence is a docs ticket.

The verdict is not the finding. absent on a mandatory requirement is a finding; absent on a sentence describing a roadmap item is not. Deciding which is which is what this skill is for, and the workflow hands you the evidence to decide it with.

The target does not have to be a contract

The question is the same everywhere — what does this requirement demand, where would it be enforced, is it enforced on every path — but what counts as a specification and where enforcement hides both change. DOMAIN_NOTES.md maps that across contracts, C and C++, services, and decompiled firmware, and covers the case where the specification is an RFC or a standard rather than a project document. Read it when the target is not a contract, and when scoping a check against a large standard.

Reference

  • ANALYSIS_FORMAT.md — the on-disk format for a per-requirement analysis. Read when extending this plugin or judging whether a record is trustworthy.

  • WORKED_EXAMPLE.md — three requirements chased to a verdict, one per verdict that is easy to get wrong: arithmetic that satisfies a requirement it does not resemble, an absence whose searches are the finding, and enforcement present on every path but the one nobody tested.

  • DOMAIN_NOTES.md — per-domain mapping of specifications and enforcement.

  • DIVERGENCE_RUBRIC.md — severity, and the two directions of a gap.

Files

resources/WORKED_EXAMPLE.md

Worked Examples

Three requirements against real code shapes, one per verdict that is easy to get wrong. Read these for calibration on how far to chase a requirement before deciding, not as a template to fill in.


implemented — arithmetic that satisfies a requirement it does not resemble

"The protocol charges a fixed 0.3% fee on the input amount for every swap." — Whitepaper §4.2

// Router.sol:L108
uint256 amountInWithFee = amountIn * 997;
// Router.sol:L110-L111
amountOut = (amountInWithFee * reserveOut) / (reserveIn * 1000 + amountInWithFee);

Nothing here contains fee, 0.3, or 30. Searching the document's vocabulary finds the comment and stops.

The verdict rests on the arithmetic: the input is scaled by 997 and the denominator by 1000, so the fee is 3/1000 = 0.3%. Then three things decide whether it is implemented rather than partial. It is applied before the output is computed, so it cannot be bypassed by the caller. It is a literal rather than a storage read, so no admin path changes it. And there is no branch around it — every swap path passes through L108.

Record the equivalence in the analysis. The next reader should not have to rederive that 997/1000 is 0.3%, and a divergence found later in the same formula will be checked against this note.

The mistake to avoid: reporting this as undecidable or absent because the fee is not named. Verify arithmetic as arithmetic.


absent — the searches are the finding

"All swap operations MUST enforce a maximum slippage of 1% between expected and actual output." — Whitepaper §4.1

// RouterV1.sol:L45
function swap(address tokenIn, address tokenOut, uint256 amountIn) external

The signature carries no minAmountOut, so there is nothing for the caller to express a tolerance with. That observation alone is suggestive, not conclusive — enforcement could compute the bound internally from an oracle.

What makes the verdict credible is the record:

  • slippage → 0 hits in RouterV1.sol

  • minAmount, minOut, limitPrice, maxDelta → 0 hits (the document's word is not the code's word, so the synonyms are checked too)

  • require, revert in swap → 2 hits, both at L47-L48 on amountIn > 0 and tokenIn != tokenOut

  • modifiers on swap → nonReentrant only

  • oracle or TWAP reads → none in the file

  • calculateSwapOutput (the one callee) → read in full; computes output, enforces nothing

  • callers of swap → none in scope; it is an entrypoint

Six places it could have been, none of them holding it. That is an absence. Without the list it is a guess in citation format.

The mistake to avoid: concluding absent after searching only the document's own vocabulary.


partial — enforcement that exists on the path nobody tested

"The parser MUST reject any frame whose declared length exceeds the remaining buffer." — RFC §4.3

/* proto.c:L112-L124 */
int parse_frame(const uint8_t *buf, size_t len, frame_t *out) {
    if (len < HDR) return -1;
    uint32_t declared = read_u32(buf);
    if (buf[4] & FLAG_CONT) {
        out->len = declared;          /* L118 — no comparison against len */
        return 0;
    }
    if (declared > len - HDR) return -1;
    out->len = declared;
    return 0;
}

The bound is enforced at L121, so a reader who finds that check marks the requirement satisfied and moves on. The continuation branch returns success at L119 having written out->len from attacker-controlled bytes without comparing it to anything.

Two paths, one enforcing and one not, is partial — and the analysis has to name which. contradicted would overstate it, because the requirement does hold for the common case; implemented would miss the finding entirely. Then check the callers, because a caller that validates before calling would close it, and one that trusts out->len after a zero return confirms it.

Also check the other build configurations. If FLAG_CONT handling is behind #ifdef, say which configuration was read.

The mistake to avoid: stopping at the first check that matches the requirement. The first check is usually the one on the path everyone tests.

Requirements and compatibility

Works with: Claude Code, Claude apps, OpenAI Codex, GitHub Copilot, Cursor, Gemini CLI, Kiro, OpenCode, Goose, Amp, Roo Code, JetBrains Junie, Factory Droid, Devin (ex-Windsurf), Mistral Vibe, OpenHands, Letta

“Works with” means the tool reads the open Agent Skills format; a skill written for one tool may use features others lack.

Needs: Declares allowed tools

Security

What our scanner noticed· Medium risk

  • Zero-width Unicode characters

A static scan is not a guarantee. Skills are third-party content: review a skill before you let an agent use it.

Attribution and licence

Published by
Trail of Bits
Publisher
Trail of Bits (Official)
Source
trailofbits/skills · plugins/spec-to-code-compliance/skills/spec-to-code-compliance · commit e4dd0bb
Licence
Creative Commons Attribution-ShareAlike 4.0 International (redistribution allowed)
  • LICENSE (added by AutoGineer from LICENSE)
  • ATTRIBUTION.md (written by AutoGineer)
Synced

AutoGineer is not affiliated with or endorsed by Trail of Bits or Trail of Bits.

Download ZIP

The ZIP holds the skill’s files, its licence files and an ATTRIBUTION.md. Download spec-to-code-compliance.zip