Verification Boundary Reporter

Analyze formal verification artifacts and produce clear reports on what is verified, what is assumed, and what remains unverified.

Overview

When working with formally verified code, it's critical to understand exactly what guarantees the verification provides and where the boundaries lie. This skill analyzes verification artifacts and produces structured reports that:

1. Identify verified components - Code with completed proofs
2. List assumptions and axioms - What is taken on trust
3. Document the trusted computing base (TCB) - External dependencies
4. Highlight unverified components - Gaps in verification coverage
5. Explain verification limitations - Why certain parts aren't verified

Core principle: Be conservative and explicit. Never overstate verification coverage.

Analysis Workflow

Verification Artifacts
    ↓
Parse & Identify Components
    ↓
Classify Each Component
    ↓
Analyze Dependencies
    ↓
Generate Boundary Report

Component Classification

Verified Components

Definition: Code with complete, checked proofs of stated properties.

Criteria:

• All proof obligations discharged
• No sorry, admit, Admitted in proofs
• Proof checked by verifier (Isabelle, Coq, Dafny, etc.)
• Properties explicitly stated and proven

Example identification:

(* VERIFIED *)
theorem insertion_sort_correct:
  "sorted (insertion_sort xs) ∧ mset (insertion_sort xs) = mset xs"
proof (induction xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  then show ?case using insert_sorted mset_insert by auto
qed

Assumed Components

Definition: Statements accepted without proof.

Criteria:

• Marked with axiom, sorry, admit, Admitted, assume
• Declared without proof
• Explicitly stated as assumptions

Example identification:

(* ASSUMED *)
Axiom functional_extensionality : forall A B (f g : A -> B),
  (forall x, f x = g x) -> f = g.

(* ASSUMED - proof incomplete *)
Theorem complex_property : ...
Proof.
  (* ... *)
Admitted.

Trusted Computing Base (TCB)

Definition: External components that must be trusted.

Components:

• Proof assistant kernel (Isabelle, Coq, Dafny verifier)
• Standard libraries used without verification
• Code extraction/generation tools
• Operating system and hardware
• External functions or FFI calls

Example identification:

(* TCB: Relies on Isabelle kernel *)
export_code my_function in SML file "output.sml"

(* TCB: Uses unverified standard library *)
definition process_file :: "string ⇒ unit" where
  "process_file path = ..." (* Calls OS file operations *)

Unverified Components

Definition: Code without formal verification.

Reasons:

• Not yet verified (work in progress)
• Intentionally left unverified (low criticality)
• Cannot be verified (external dependencies)
• Verification attempted but incomplete

Example identification:

// UNVERIFIED: No method body verification
method ProcessData(input: seq<int>) returns (output: seq<int>)
  // No ensures clause - postcondition not specified
{
  // Implementation without verification
}

Analysis Process

Step 1: Identify All Components

Scan verification artifacts for:

• Definitions and implementations
• Theorems and lemmas
• Axioms and assumptions
• External dependencies
• Extracted/generated code

Step 2: Check Verification Status

For each component, determine:

• Is there a proof? (Complete/incomplete/absent)
• Are there assumptions or axioms?
• What properties are claimed?
• What properties are proven?

Step 3: Trace Dependencies

Map dependencies to understand:

• What verified code depends on
• Assumption propagation
• TCB elements used
• Unverified code interactions

Step 4: Assess Coverage

Calculate:

• Percentage of code verified
• Critical vs non-critical components
• Verification depth (shallow vs deep properties)

Step 5: Generate Report

Produce structured Markdown report with:

• Executive summary
• Verified components list
• Assumptions and axioms
• TCB documentation
• Unverified components
• Verification gaps and limitations

Report Structure

Template

# Verification Boundary Report

**Project:** [Name]
**Date:** [Date]
**Verifier:** [Isabelle/Coq/Dafny/etc.]
**Analyst:** [Name]

## Executive Summary

[Brief overview of verification coverage and key findings]

## Verification Statistics

- Total components: X
- Verified: Y (Z%)
- Assumed: A
- Unverified: B
- TCB elements: C

## Verified Components

### [Component Name]

**Location:** [File:Line]
**Properties Proven:**
- [Property 1]
- [Property 2]

**Proof Status:** ✓ Complete
**Dependencies:** [List verified dependencies]

## Assumptions and Axioms

### [Assumption Name]

**Location:** [File:Line]
**Statement:** [Formal statement]
**Justification:** [Why this is assumed]
**Impact:** [What depends on this]
**Risk Level:** [Low/Medium/High]

## Trusted Computing Base

### [TCB Element]

**Type:** [Kernel/Library/Tool/OS/Hardware]
**Description:** [What is trusted]
**Justification:** [Why it must be trusted]
**Mitigation:** [How risk is managed]

## Unverified Components

### [Component Name]

**Location:** [File:Line]
**Reason:** [Why unverified]
**Risk Assessment:** [Impact if incorrect]
**Recommendation:** [Should it be verified?]

## Verification Gaps

[List areas where verification is incomplete or absent]

## Limitations

[Explicit statement of what the verification does NOT guarantee]

## Recommendations

[Suggestions for improving verification coverage]

Framework-Specific Analysis

Isabelle/HOL Analysis

For Isabelle-specific verification boundary analysis, see references/isabelle_analysis.md.

Key aspects:

• Identifying sorry and incomplete proofs
• Checking axiom usage
• Analyzing code generation trust
• Sledgehammer and automation reliance

Coq Analysis

For Coq-specific verification boundary analysis, see references/coq_analysis.md.

Key aspects:

• Identifying Admitted and admit
• Checking axiom usage (functional extensionality, etc.)
• Analyzing extraction trust
• Program obligations

Dafny Analysis

For Dafny-specific verification boundary analysis, see references/dafny_analysis.md.

Key aspects:

• Checking method verification
• Identifying assume statements
• Analyzing external methods
• Verification timeout issues

Common Patterns

For common verification boundary patterns and red flags, see references/boundary_patterns.md.

Patterns include:

• Assumption propagation
• Partial verification
• Verification by testing
• Trusted wrappers
• Verification escape hatches

Example Analysis

Input: Verified sorting implementation

theory VerifiedSort
imports Main "HOL-Library.Multiset"
begin

fun insert :: "nat ⇒ nat list ⇒ nat list" where
  "insert x [] = [x]" |
  "insert x (y # ys) = (if x ≤ y then x # y # ys else y # insert x ys)"

fun insertion_sort :: "nat list ⇒ nat list" where
  "insertion_sort [] = []" |
  "insertion_sort (x # xs) = insert x (insertion_sort xs)"

lemma insert_sorted:
  "sorted xs ⟹ sorted (insert x xs)"
  by (induction xs) auto

lemma mset_insert:
  "mset (insert x xs) = {#x#} + mset xs"
  by (induction xs) (auto simp: ac_simps)

theorem insertion_sort_correct:
  "sorted (insertion_sort xs) ∧ mset (insertion_sort xs) = mset xs"
  by (induction xs) (auto simp: insert_sorted mset_insert)

export_code insertion_sort in SML file "sort.sml"

end

Output: Verification Boundary Report

# Verification Boundary Report

**Project:** VerifiedSort
**Date:** 2026-02-17
**Verifier:** Isabelle/HOL
**Analyst:** Verification Boundary Reporter

## Executive Summary

The insertion sort implementation is fully verified with complete proofs of
correctness (sorting and p