Spec-to-Code Compliance

Verify that code implements exactly what documentation specifies through deterministic, evidence-based alignment analysis. Designed for blockchain audits where spec-to-code divergence can lead to critical vulnerabilities.

Overview

The Spec-to-Code Compliance plugin performs systematic comparison between specification documents (whitepapers, design docs) and actual implementation code, producing audit-grade compliance reports with:

Zero speculation - Every claim backed by exact quotes or line numbers
Structured IR workflow - Spec Intent → Code Behavior → Alignment → Divergence
Confidence scoring - All mappings include 0-1 confidence scores
Exploit scenarios - Critical findings include attack vectors and economic impact

This plugin is designed for blockchain audits where formal specifications exist. It requires both specification documents AND corresponding implementation code.

When to Use

Protocol Audits

Smart contracts being verified against whitepapers or protocol specifications

Compliance Checks

Finding gaps between intended behavior and actual implementation

Spec Divergence

Identifying undocumented code behavior or unimplemented spec claims

Documentation Drift

Discovering where code has evolved beyond original design documents

Concrete Triggers

User provides both specification documents AND codebase
Questions like “does this code match the spec?” or “what’s missing from the implementation?”
Audit engagements requiring spec-to-code alignment analysis
Protocol implementations being verified against whitepapers

When NOT to Use

Do NOT use this plugin for:

Codebases without corresponding specification documents
General code review or vulnerability hunting (use other audit plugins)
Writing or improving documentation (this only verifies compliance)
Non-blockchain projects without formal specifications

Analysis Workflow

The plugin executes a rigorous 7-phase workflow:

Documentation Discovery

Identifies all spec sources (whitepapers, READMEs, design notes, Notion exports, meeting transcripts)

Format Normalization

Converts PDF, Markdown, DOCX, HTML, TXT to clean canonical format preserving structure

Spec Intent IR

Extracts all intended behavior (invariants, formulas, flows, security requirements) into structured Spec-IR

Code Behavior IR

Line-by-line semantic analysis of implementation producing Code-IR with full traceability

Alignment IR

Compares Spec-IR to Code-IR, generates alignment records with match types and confidence scores

Divergence Classification

Categorizes misalignments by severity (Critical/High/Medium/Low) with exploit scenarios

Final Report

Produces audit-grade compliance report with evidence links and remediation guidance

Match Types

The plugin classifies spec-to-code alignment into six categories:

Match Type	Description	Example
`full_match`	Code exactly implements spec	Spec says “revert if balance < amount”, code has exact check
`partial_match`	Incomplete implementation	Spec requires 3 checks, code implements 2
`mismatch`	Spec says X, code does Y	Spec says “use safe math”, code uses unchecked arithmetic
`missing_in_code`	Spec claim not implemented	Spec documents access control, code has none
`code_stronger_than_spec`	Code adds behavior beyond spec	Code has reentrancy guard not in spec
`code_weaker_than_spec`	Code misses requirements	Spec requires signature verification, code skips it

Severity Classification

Critical
High
Medium
Low

Indicators:

Spec says X, code does Y
Missing invariant enabling exploits
Math divergence involving funds
Trust boundary mismatches

Example:

// Spec: "Transfer must revert if balance insufficient"
// Code: Transfers without balance check (critical vulnerability)

Indicators:

Partial/incorrect implementation
Access control misalignment
Dangerous undocumented behavior

Example:

// Spec: "Only owner can withdraw"
// Code: Missing onlyOwner modifier (high severity)

Indicators:

Ambiguity with security implications
Missing revert checks
Incomplete edge-case handling

Example:

// Spec: "Handle zero address"
// Code: No zero address check (medium severity)

Indicators:

Documentation drift
Minor semantics mismatch
Non-security divergence

Example:

// Spec: "Emit Transfer event"
// Code: Event name is TransferExecuted (low severity)

IR Structure Examples

Spec-IR Record

spec_id: SPEC-001
spec_excerpt: "The swap function must verify that outputAmount >= minOutput before executing the trade"
source_section: "Section 3.2: Slippage Protection"
semantic_type: precondition
normalized_intent:
  function: swap
  precondition: "outputAmount >= minOutput"
  enforcement: "must revert if violated"
confidence: 0.95

Code-IR Record

code_id: CODE-001
file: contracts/DEX.sol
lines: 142-145
function: swap
semantic_type: precondition_check
code_excerpt: |
  require(outputAmount >= minOutput, "Slippage exceeded");
behavior:
  check: "outputAmount >= minOutput"
  action_on_violation: revert
  error_message: "Slippage exceeded"

Alignment Record

alignment_id: ALIGN-001
spec_id: SPEC-001
code_id: CODE-001
match_type: full_match
confidence: 0.98
reasoning: |
  Spec requires "outputAmount >= minOutput" precondition with revert.
  Code implements exact check with require statement.
  Error message provides user-friendly context.
evidence:
  spec_quote: "must verify that outputAmount >= minOutput before executing"
  code_location: "contracts/DEX.sol:142-145"

Divergence Finding (Critical)

finding_id: DIV-CRIT-001
severity: critical
match_type: missing_in_code
spec_requirement: |
  Section 4.1: "All external calls must update state before calling
  external contracts to prevent reentrancy attacks"
code_behavior: |
  contracts/Vault.sol:78-82 - withdraw() makes external call before
  updating user balance, enabling reentrancy
exploit_scenario: |
  Attacker can recursively call withdraw() before balance is updated,
  draining vault funds:
  1. Attacker calls withdraw(100)
  2. Line 80: vault.transfer(msg.sender, amount)
  3. Attacker's fallback calls withdraw(100) again
  4. Balance still shows 100, transfer succeeds
  5. Repeat until vault drained
economic_impact: "Complete loss of vault funds (~$2M TVL)"
remediation: |
  Update state before external call (checks-effects-interactions pattern):
  balances[msg.sender] -= amount;  // Move before transfer
  vault.transfer(msg.sender, amount);
confidence: 0.95

Anti-Hallucination Requirements

Zero-speculation rules enforced throughout analysis:

If spec is silent: classify as UNDOCUMENTED
If code adds behavior: classify as UNDOCUMENTED CODE PATH
If unclear: classify as AMBIGUOUS
Every claim must quote original text or line numbers
No inference from prior knowledge of protocols

Rationalizations to Reject

The plugin rejects these common shortcuts:

Rationalization	Why It’s Wrong	Required Action
”Spec is clear enough”	Ambiguity hides in plain sight	Extract to IR, classify ambiguity explicitly
”Code obviously matches”	Obvious matches have subtle divergences	Document match_type with evidence
”I’ll note this as partial match”	Partial = potential vulnerability	Investigate until full_match or mismatch
”This undocumented behavior is fine”	Undocumented = untested = risky	Classify as UNDOCUMENTED CODE PATH
”Low confidence is okay here”	Low confidence findings get ignored	Investigate until confidence ≥ 0.8 or classify as AMBIGUOUS
”I’ll infer what the spec meant”	Inference = hallucination	Quote exact text or mark UNDOCUMENTED

Output Report Structure

The final compliance report includes:

Executive Summary - Finding counts, overall compliance metrics
Documentation Sources - All spec documents analyzed
Spec Intent Breakdown - Extracted Spec-IR with full citations
Code Behavior Summary - Code-IR semantic map
Full Alignment Matrix - Every spec item mapped to code status
Divergence Findings - Critical/High/Medium/Low with evidence
Missing Invariants - Spec requirements not implemented
Incorrect Logic - Code behavior contradicting spec
Math Inconsistencies - Formula divergence
Flow Mismatches - State machine divergence
Access Control Drift - Permission misalignment
Undocumented Behavior - Code paths not in spec
Ambiguity Hotspots - Unclear spec or code sections
Recommendations - Remediation guidance
Documentation Updates - Suggested spec improvements
Final Risk Assessment - Overall compliance rating

Quality Standards

Spec-IR Completeness

All invariants extracted and normalized
All formulas in canonical symbolic form
All security requirements documented
Minimum 80% confidence on critical items

Code-IR Completeness

Every function analyzed with control flow
All state changes tracked
All external calls documented
Line numbers for all evidence

Alignment Quality

Every spec item has alignment record
Match types accurately classified
Confidence scores justified
Evidence links verified

Divergence Findings

Exploit scenarios for critical issues
Economic impact analysis
Remediation with code examples
Citations to both spec and code

Agent Usage

The spec-compliance-checker agent performs the full 7-phase workflow autonomously:

# Invoke the agent directly
"Use the spec-compliance-checker agent to verify this codebase against the whitepaper."

The agent produces:

Structured IR artifacts (Spec-IR, Code-IR, Alignment-IR)
Divergence findings with severity classification
Final compliance report in markdown format

Example Use Cases

DeFi Protocol Audit

Whitepaper specifies constant product formula x * y = k. Code uses x * y = k + fee, enabling economic exploit.

Governance Compliance

Spec requires 7-day timelock on proposals. Code implements 3-day timelock, violating governance security model.

Access Control Gap

Documentation describes admin-only emergency pause. Implementation missing onlyAdmin modifier.

Undocumented Upgrade

Code implements proxy upgrade pattern not mentioned in specification, introducing trust assumptions.

The plugin includes detailed reference documentation:

resources/IR_EXAMPLES.md - Complete IR workflow examples with DEX patterns
resources/OUTPUT_REQUIREMENTS.md - IR production standards and quality thresholds
resources/COMPLETENESS_CHECKLIST.md - Verification checklist for all phases

Integration Points

Property-Based Testing - Verify extracted invariants hold in practice
Zeroize Audit - Cross-check sensitive data handling against spec
Constant-Time Analysis - Validate timing requirements from spec

Author: Omar Inuwa (Trail of Bits)Version: 1.1.0

Get Started

Core Concepts

Smart Contract Security

Code Auditing

Static Analysis Tools

Verification & Testing

Specialized Tools

Development

Infrastructure & Tools

Other

Overview

When to Use

Protocol Audits

Compliance Checks

Spec Divergence

Documentation Drift

Concrete Triggers

When NOT to Use

Analysis Workflow

Match Types

Severity Classification

IR Structure Examples

Spec-IR Record

Code-IR Record

Alignment Record

Divergence Finding (Critical)

Anti-Hallucination Requirements

Rationalizations to Reject

Output Report Structure

Quality Standards

Agent Usage

Example Use Cases

DeFi Protocol Audit

Governance Compliance

Access Control Gap

Undocumented Upgrade

Integration Points

Build docs developers (and LLMs) love

Get Started

Core Concepts

Smart Contract Security

Code Auditing

Static Analysis Tools

Verification & Testing

Specialized Tools

Development

Infrastructure & Tools

Other

​Overview

​When to Use

Protocol Audits

Compliance Checks

Spec Divergence

Documentation Drift

​Concrete Triggers

​When NOT to Use

​Analysis Workflow

​Match Types

​Severity Classification

​IR Structure Examples

​Spec-IR Record

​Code-IR Record

​Alignment Record

​Divergence Finding (Critical)

​Anti-Hallucination Requirements

​Rationalizations to Reject

​Output Report Structure

​Quality Standards

​Agent Usage

​Example Use Cases

DeFi Protocol Audit

Governance Compliance

Access Control Gap

Undocumented Upgrade

​Related Resources

​Integration Points

Build docs developers (and LLMs) love

Overview

When to Use

Concrete Triggers

When NOT to Use

Analysis Workflow

Match Types

Severity Classification

IR Structure Examples

Spec-IR Record

Code-IR Record

Alignment Record

Divergence Finding (Critical)

Anti-Hallucination Requirements

Rationalizations to Reject

Output Report Structure

Quality Standards

Agent Usage

Example Use Cases

Related Resources

Integration Points