/attest

Verification Methods

Purpose: Read this when choosing static verification techniques, assigning per-criterion verdicts, formatting evidence, or deciding when to route to runtime verification.

Contents

• Verification approach
• Verification methods
• Verdict assignment
• Evidence format
• Confidence scoring
• Resource allocation guideline

Verification Approach

Attest performs static verification. It does not execute the system.

What Attest Can Verify

What Requires Runtime Verification

Mark these as NOT_TESTED with a runtime verification plan.

Verification Methods

Must-Keep Absence Pattern

Criterion: AC-LOGIN-007 "Account lockout after 5 failed attempts"
Search locations:
  - src/controllers/auth.ts
  - src/middleware/auth.ts
  - src/models/user.ts
Result:
  No lockout logic found
Verdict:
  FAIL

Verdict Assignment

Per-Criterion Verdicts

Decision Flow

1. Can the criterion be verified statically?
   -> No: NOT_TESTED
   -> Yes:
      2. Does implementation evidence exist?
         -> No: FAIL
         -> Yes:
            3. Does it match the specification fully?
               -> Fully: PASS
               -> Partially: PARTIAL
               -> Contradicts: FAIL

Evidence Format

EVIDENCE:
  criterion_id: AC-LOGIN-001
  verdict: PASS
  method: CODE_SEARCH + LOGIC_TRACE
  references:
    - file: src/routes/auth.ts
      line: 42
      snippet: "router.post('/api/auth/login', authController.login)"
      relevance: "Endpoint definition matching spec"
    - file: src/controllers/auth.ts
      line: 78-95
      snippet: "async login(req, res) { ... }"
      relevance: "Handler validates email + password"
  gaps: []
  notes: "Implementation matches spec."

Gap Description for PARTIAL / FAIL

EVIDENCE:
  criterion_id: AC-LOGIN-007
  verdict: FAIL
  method: ABSENCE_CHECK
  references: []
  gaps:
    - type: MISSING_IMPLEMENTATION
      description: "Account lockout mechanism not found"
      spec_requirement: "Lock account after 5 failed login attempts"
      searched_locations:
        - src/controllers/auth.ts
        - src/middleware/auth.ts
        - src/models/user.ts
      impact: CRITICAL
  notes: "No login attempt tracking or lockout logic exists in codebase"

Confidence Scoring

Rule: when confidence < 0.5, mark the result as NOT_TESTED with a runtime recommendation.

Resource Allocation Guideline

When scope must be reduced, finish all CRITICAL criteria first, then HIGH, then sampled MEDIUM. Defer LOW to AUDIT mode before reducing higher priorities.

Static Methods + Runtime-Only Areas (SKILL.md excerpt)

Runtime-Only Areas

Route these to NOT_TESTED with a runtime plan:

• Performance thresholds
• Concurrency behavior
• Visual rendering
• External API integration
• UX quality