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:

Identify verified components - Code with completed proofs
List assumptions and axioms - What is taken on trust
Document the trusted computing base (TCB) - External dependencies
Highlight unverified components - Gaps in verification coverage
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](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](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](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](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

verification-boundary-reporter

Como adicionar

Cole no README do seu repo

Skills relacionadas

pdf

theme-factory

pptx

canvas-design

Receba novas skills de Documentos toda segunda