Spec-to-Code Compliance

Evidence-based alignment analysis between specifications and blockchain implementations

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:

1. Documentation Discovery

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

2. Format Normalization

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

3. Spec Intent IR

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

4. Code Behavior IR

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

5. Alignment IR

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

6. Divergence Classification

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

7. 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

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)

High

Indicators:

• Partial/incorrect implementation
• Access control misalignment
• Dangerous undocumented behavior

Example:

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

Medium

Indicators:

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

Example:

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

Low

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:

1. Executive Summary - Finding counts, overall compliance metrics
2. Documentation Sources - All spec documents analyzed
3. Spec Intent Breakdown - Extracted Spec-IR with full citations
4. Code Behavior Summary - Code-IR semantic map
5. Full Alignment Matrix - Every spec item mapped to code status
6. Divergence Findings - Critical/High/Medium/Low with evidence
7. Missing Invariants - Spec requirements not implemented
8. Incorrect Logic - Code behavior contradicting spec
9. Math Inconsistencies - Formula divergence
10. Flow Mismatches - State machine divergence
11. Access Control Drift - Permission misalignment
12. Undocumented Behavior - Code paths not in spec
13. Ambiguity Hotspots - Unclear spec or code sections
14. Recommendations - Remediation guidance
15. Documentation Updates - Suggested spec improvements
16. 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.

Related Resources

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