Verification Scaffold Skill

Verification Scaffold Skill for Claude

When to Use This Skill

Activate when: generating verification checklists from threat findings, creating SVA assertion templates, building security review checklists, planning verification coverage, mapping threats to verification tiers, producing artifacts for security review boards, creating Tier 1 assertion templates.

Do not use for: production-ready SVA (templates only, not production IP), formal verification setup, RTL code review (v2 roadmap), threat identification (threat-model-skill), compliance gap analysis (compliance-pipeline-skill), executive communication (executive-brief-skill), functional verification beyond security.

Scope Constraints

Read files ONLY within project working directory. No home directory dotfiles, external services, shell commands, or file modifications. Output SVA templates as text only in the VerificationChecklist format.

Input Sanitization

Reject path traversal (../), shell metacharacters, paths outside project directory. RTL signal names: alphanumeric, underscores, brackets only.

Core Principles

1. Scaffolds, Not Solutions

Every artifact is a starting point. SVA templates require signal-level customization. NL properties require formalization. Spec references require contextual interpretation. The scaffold saves time; it does not replace expertise.

2. Honest Annotation Over False Precision

Every assertion includes two mandatory annotations:

• // INTENT: — What this assertion checks
• // DOES NOT CHECK: — What it explicitly does NOT verify

These exist because a template that appears comprehensive but silently omits key scenarios is more dangerous than one that declares its limitations. False coverage is worse than known gaps.

3. Tier Discipline

Attempting SVA for Tier 3 properties produces false confidence because these require specialized formal methods, physical measurement, or architectural review. The skill refuses to generate SVA for Tier 3.

4. Confidence Propagation

Verification items inherit confidence from their upstream ThreatFinding. A SPECULATIVE threat cannot produce a GROUNDED verification item.

ThreatFinding.confidenceTier → VerificationItem.upstreamConfidence
VerificationItem.verificationConfidence = min(upstreamConfidence, tierConfidence)

Where tierConfidence is: Tier 1 = HIGH, Tier 2 = MEDIUM, Tier 3 = REFERENCE.

A GROUNDED threat verified by a Tier 2 property gets MEDIUM overall confidence. A SPECULATIVE threat verified by a Tier 1 assertion gets SPECULATIVE overall confidence (upstream caps it).

5. Template vs. Ready

• [TEMPLATE] — Placeholder signal names, requires design-specific customization
• [READY] — Actual RTL signal names provided by engineer, ready for syntax review

Most will be [TEMPLATE] because the skill typically lacks RTL access. [READY] only when engineer provides signal names, module hierarchy, and clock/reset info.

6. Never "Correct" — Always "Candidate"

Every assertion is framed as: "Candidate assertion for review. Verify against your RTL before use." This framing is not optional — it appears in caveat blocks, annotations, and handoff notes.

References

Load skill-specific references as needed:

Input Requirements

Required: (1) ThreatFindings from threat-model-skill — id, severity, confidenceTier, attackSurface, verificationMethod per finding, plus DocumentEnvelope with attack surface checklist and confidence summary. (2) Verification Scope — which threats (all/specific IDs/filtered), target tier(s), output format (checklist/templates/both).

Optional (improve quality): (3) RTL Signal Information — enables [READY] assertions: module hierarchy, clock/reset, security-critical signals, address ranges. (4) Existing Verification Assets — prevents duplication. (5) Design Constraints — clock domains, reset architecture, tool constraints.

Input Validation

[x/!/?] ThreatFindings envelope present with valid confidence summary
[x/!/?] At least one ThreatFinding entity with verificationMethod field
[x/!/?] Attack surface checklist present (for coverage mapping)
[x/!/?] RTL signal information available (improves template specificity)
[x/!/?] Existing verification assets listed (prevents duplication)

Legend: [x] = present, [!] = missing (required), [?] = missing (optional)

If ThreatFindings missing: request threat-model-skill first or provide threat descriptions manually. Without ThreatFindings, the skill cannot map threats to tiers, propagate confidence, or generate targeted templates.

Progress Tracking

Copy this checklist and update as you complete each phase:

Progress:
- [ ] Phase 1: Input Analysis & Tier Assignment
- [ ] Phase 2: Tier 1 — SVA Assertion Template Generation
- [ ] Phase 3: Tier 2 — Natural-Language Property Description
- [ ] Phase 4: Tier 3 — Specification-Only Descriptions
- [ ] Phase 5: Output Assembly & Coverage Mapping

Recovery note: If context has been compacted and you've lost prior step details, check the progress checklist above. Resume from the last unchecked item. Re-read the relevant reference file for that phase.

The Verification Scaffold Process

Phase 1: Tier Assignment -> Phase 2: Tier 1 SVA -> Phase 3: Tier 2 NL -> Phase 4: Tier 3 Spec -> Phase 5: Output Assembly

Phase 1: Input Analysis & Tier Assignment

Validate ThreatFindings. Per finding: note confidenceTier (propagates), verificationMethod (informs tier), severity (priority).

Tier Assignment Tables

Tier 1 — Mechanical / Structural (SVA Templates)

Tier 2 — Protocol / Behavioral (NL Properties)

Tier 3 — Specification-Only (No SVA)

Assignment Rules:

1. verificationMethod = "SVA" -> Tier 1
2. "simulation" + behavioral -> Tier 2
3. "review"/"formal-analysis" -> Tier 2 or 3 by property type
4. "test" + physical measurement -> Tier 3
5. Information flow or side-channel -> always Tier 3 because these cannot be expressed as signal-level assertions
6. When uncertain, assign higher tier — under-promising is safer

Tier Assignment Plan

Verification Scaffold Plan
===========================
Source: [TM-ID] — [N] ThreatFindings consumed
Tier 1 (SVA): [N] — [IDs]  |  Tier 2 (NL): [N] — [IDs]
Tier 3 (Spec): [N] — [IDs]  |  Not Verifiable: [N] — [IDs + reason]
RTL Signals: [AVAILABLE/NOT] — Assertions: [READY/TEMPLATE]
Priority: CRITICAL -> HIGH -> MEDIUM -> LOW

Wait for engineer confirmation before proceeding.

Phase 2: Tier 1 — SVA Assertion Template Generation

Refer to references/sva-authoring-guide-syntax.md and references/sva-authoring-guide-annotations.md for authoring rules.

Step 2.1: Pattern Selection

Step 2.2: Assertion Template Structure

// =============================================================================
// Verification Item: [VI-TM-YYYY-NNN-MMM]
// Source Threat: [TF-TM-YYYY-NNN-XXX] — [threat title]
// Tier: 1 | Status: [TEMPLATE/READY] | Confidence: [upstream] -> [computed]
// =============================================================================
// INTENT: [specific description]
// DOES NOT CHECK: [specific omissions]
// CANDIDATE FOR REVIEW: Verify against your RTL before use.

module sva_[name] (input logic <clk>, <rst_n>, <signals...>);
  property p_[name];
    @(posedge <clk>) disable iff (!<rst_n>)
    <antecedent> |-> <consequent>;
  endproperty
  a_[name]: assert property (p_[name])
    else $error("[VI-ID] FAIL: [message]");
  c_[name]_trigger: cover property (@(posedge <clk>) <antecedent>);
endmodule

Step 2.3: Mandatory Annotations

Every assertion MUST include // INTENT: (what is checked and why) and // DOES NOT CHECK: (specific omissions). See pattern library for examples.

Step 2.4: SVA Pattern Library

-> Load references/sva-pattern-library.md for the 7 standard SVA patterns (access control gate, FSM transition guard, register lock, address range, one-hot, mutual exclusion, handshake timeout).

Phase 3: Tier 2 — Natural-Language Property Description

For each Tier 2 finding, produce:

### [VI-TM-YYYY-NNN-MMM] — [Property Title]
**Source:** [TF-ID] | **Tier:** 2 | **Confidence:** [upstream] -> MEDIUM

**Property Statement:** [temporal NL: "Before X, Y must have completed" / "While S, P holds" / "If E, within N cycles R occurs"]
**Verification Approach:** [simulation / constrained random / protocol checker / formal / review]
**Checks:** [2-3 sentences]  **Does NOT Check:** [2-3 sentences]
**Test Scenarios:** 1. Normal operation 2. Attack scenario 3. Edge case
**Formalization Notes:** [SVA feasibility + what info needed]

-> Load references/sva-pattern-library.md for domain-specific Tier 2 patterns (DICE layer ordering, TDISP state machine, CXL IDE key rotation, SPDM authentication).

Phase 4: Tier 3 — Specification-Only Descriptions

For each Tier 3 finding, produce:

### [VI-TM-YYYY-NNN-MMM] — [Property Title]
**Source:** [TF-ID] | **Tier:** 3 | **Confidence:** REFERENCE
**NO SVA — RATIONALE:** [specific reason SVA cannot express this]
**Property:** [spec description with section reference]
**Methodology:** [specific method, tool, expertise needed]
**Spec Reference:** [standard, version, section, quoted requirement]
**Review Checklist:** [3-5 items]

Tier 3 Categories:

Phase 5: Render & Coverage Mapping

DocumentEnvelope

type: verification-checklist
id: "VC-[YYYY]-[NNN]"
title: "Verification Scaffold — [Component] [Domain(s)]"
created/updated: "[YYYY-MM-DD]"
soc-family: ["[family]"]
technology-domain: ["[domain]"]
standards: ["[standard]"]
related-documents: ["[TM-YYYY-NNN]"]
status: "draft"
confidence-summary: { grounded: N, inferred: N, speculative: N, absent: N }
caveats: |
  LLM-generated scaffold. All assertions CANDIDATES FOR REVIEW.
  [TEMPLATE] requires signal customization. [READY] requires correctness review.
  Tier 3: NO SVA. NOT VERIFIED: [list gaps]

Mandatory Elements

Caveat block: LLM-generated draft notice, critical limitations ([TEMPLATE] won't compile, [READY] not formally verified, Tier 2 needs formalization, Tier 3 no artifacts), per-tier counts, specific coverage gaps.

Coverage mapping: Threat-to-VI traceability table (Threat ID, Severity, Confidence, VI ID, Tier, Status), coverage-by-attack-surface summary, explicit verification gaps with rationale.

Confidence summary: Per-tier counts with upstream confidence distribution, percentage breakdown, propagation assessment narrative.

VerificationItem Entity Format

Per entity schema at shared-references/soc-security/entity-schema.md. See worked example for structure.

Interaction Patterns

Starting: Announce the 5-phase process (tier assignment, SVA templates, NL properties, spec references, coverage mapping), then begin analyzing threat findings.

Phase transitions: Announce tier assignments confirmed, count of items generated, and what comes next.

RTL signals provided mid-session: Update affected assertions from [TEMPLATE] to [READY] with explicit signal substitution list. Note that [READY] still requires review because signal substitution does not guarantee correctness.

Finding cannot be mapped: Explain why, offer options (provide more context, accept as gap, assign to Tier 3 as minimum), recommend Tier 3 because at minimum the threat gets documented with a review checklist.

Quality Standards

1. Every Tier 1 assertion has // INTENT: and // DOES NOT CHECK: — no exceptions
2. Every assertion marked [TEMPLATE] or [READY] — none unmarked
3. No SVA for Tier 3 — skill refuses
4. Confidence propagated correctly — no VI exceeds source threat confidence
5. Coverage mapping complete — every ThreatFinding in traceability table
6. Gaps documented with rationale
7. Caveat block tailored, not boilerplate
8. Assertions syntactically plausible SVA
9. Annotations specific per assertion, not copy-pasted
10. Tier 2 includes normal + attack test scenarios

Good: assertions specific to threat, DOES NOT CHECK lists specific omissions, Tier 2 uses temporal language, Tier 3 explains why no SVA and what instead. Bad: missing annotations, SVA for Tier 3, all [READY] without RTL, missing coverage mapping, no gaps documented.

Worked Example: TDISP Device Assignment

Input: TM-2026-001 — TDISP Device Assignment Module Threat Model (8 findings)

Phase 1 Output

Tier Assignment:
  Tier 1 (SVA): 4 findings
    TF-003 (FSM desync, CRITICAL/GROUNDED) -> FSM transition guard
    TF-005 (BAR manipulation, CRITICAL/GROUNDED) -> Address range check
    TF-006 (Register lock bypass, HIGH/GROUNDED) -> Register lock
    TF-008 (Concurrent access, MEDIUM/INFERRED) -> Mutual exclusion

  Tier 2 (NL Property): 2 findings
    TF-001 (SPDM auth bypass, HIGH/GROUNDED) -> Authentication sequence
    TF-004 (IDE key exposure, HIGH/GROUNDED) -> Key exchange protocol

  Tier 3 (Spec Only): 2 findings
    TF-002 (Timing side-channel, MEDIUM/SPECULATIVE) -> Timing analysis
    TF-007 (Cross-device info flow, HIGH/INFERRED) -> Information flow analysis

Phase 2 Output (one assertion shown)

// =============================================================================
// VI-VC-2026-001-001
// Source: TF-TM-2026-001-003 — TDISP State Machine Desynchronization
// Tier: 1 (Mechanical/Structural) | Status: [TEMPLATE] | Confidence: GROUNDED -> HIGH
// =============================================================================
// INTENT: Checks that the TDISP assignment FSM cannot transition from
//         LOCKED to DATA_TRANSFER without authentication_complete being
//         asserted in the immediately preceding cycle. This enforces the
//         TDISP 1.0 Section 4.2.1 requirement that authentication must
//         complete before data transfer begins.
//
// DOES NOT CHECK:
//   - Whether authentication_complete was legitimately derived from
//     a successful SPDM exchange (only checks the signal, not the protocol)
//   - Glitch-based state corruption that bypasses the FSM transition logic
//   - Behavior during or immediately after reset
//   - Transitions to states other than DATA_TRANSFER
//   - The correctness of the LOCKED state itself

property p_tdisp_locked_to_transfer_guard;
  @(posedge <clk>) disable iff (!<rst_n>)
  (<tdisp_state> == LOCKED) ##1 (<tdisp_state> == DATA_TRANSFER) |->
    $past(<authentication_complete>);
endproperty

a_tdisp_locked_to_transfer: assert property (p_tdisp_locked_to_transfer_guard)
  else $error("[VI-001] LOCKED->DATA_TRANSFER without authentication");

c_tdisp_locked_to_transfer_trigger: cover property (
  @(posedge <clk>) (<tdisp_state> == LOCKED) ##1 (<tdisp_state> == DATA_TRANSFER)
);

Phase 5 Output (coverage mapping)

Verification gaps: 0 threats without any coverage. 2 threats at Tier 3 only (timing side-channel, information flow) — recommended for specialized tool-based analysis.

Knowledge Base Integration

When generating scaffolds for a previously analyzed component: check for existing VerificationChecklist documents, reuse effective assertion patterns (customize signals), reference prior verification coverage, and focus new scaffold on threats not covered by existing verification.

When upstream ThreatFinding has crossFamilyReuse information: generate base template once, note family-specific deltas in annotations, create variant templates if differences are significant, document which signals change across families in placeholder descriptions.

Downstream handoff: compliance-pipeline-skill (verification items as compliance evidence), executive-brief-skill (coverage statistics for executive reporting), engineer's verification environment (assertion templates for testbench integration).