Verification Boundary Reporter

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

(* 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 *)
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.

(* 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: No method body verification
method ProcessData(input: seq<int>) returns (output: seq<int>)
  // No ensures clause - postcondition not specified
{
  // Implementation without verification
}

# 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]

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

# 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 permutation preservation). The verification relies
on Isabelle's standard library and kernel as the trusted computing base.
Code extraction to SML is part of the TCB.

## Verification Statistics

- Total components: 5
- Verified: 3 (60%)
- Assumed: 0 (0%)
- Unverified: 0 (0%)
- TCB elements: 2 (40%)

## Verified Components

### insert function
**Location:** VerifiedSort.thy:5-7
**Properties Proven:**
- Preserves sortedness (insert_sorted)
- Preserves multiset (mset_insert)
**Proof Status:** ✓ Complete
**Dependencies:** None (base case)

### insertion_sort function
**Location:** VerifiedSort.thy:9-11
**Properties Proven:**
- Produces sorted output
- Preserves all elements (permutation)
**Proof Status:** ✓ Complete
**Dependencies:** insert, insert_sorted, mset_insert

### Correctness theorem
**Location:** VerifiedSort.thy:18-19
**Statement:** sorted (insertion_sort xs) ∧ mset (insertion_sort xs) = mset xs
**Proof Status:** ✓ Complete
**Proof Method:** Induction with auto

## Assumptions and Axioms

None. All proofs are complete without axioms.

## Trusted Computing Base

### Isabelle/HOL Kernel
**Type:** Proof Assistant Kernel
**Description:** The Isabelle/HOL logical kernel that checks all proofs
**Justification:** Fundamental to all verification; cannot be verified within itself
**Mitigation:** Small, well-audited kernel; decades of use

### Isabelle Standard Library
**Type:** Library
**Description:** HOL-Library.Multiset for multiset operations
**Justification:** Used for permutation reasoning
**Mitigation:** Part of standard Isabelle distribution, widely used and tested

### Code Generation
**Type:** Tool
**Description:** export_code mechanism that generates SML
**Justification:** Translates verified Isabelle code to executable SML
**Mitigation:** Code generator is part of Isabelle, but translation correctness
is not formally verified. Generated code must be trusted to match semantics.

## Unverified Components

None. All algorithmic components are verified.

## Verification Gaps

None identified in the core algorithm.

## Limitations

1. **Code extraction trust:** The generated SML code is not verified to match
   the Isabelle semantics. The code generator is trusted.

2. **Termination:** While termination is proven by Isabelle's function package,
   the extracted code's termination depends on the SML runtime.

3. **I/O and side effects:** Any I/O operations in the extracted code are
   outside the verification boundary.

4. **Numeric representation:** The verification uses mathematical integers (nat),
   but extracted code uses machine integers which may overflow.

## Recommendations

1. **Consider verified extraction:** Use a verified code generator or
   certified compilation if higher assurance is needed.

2. **Add overflow checks:** If using extracted code with large inputs,
   add runtime checks for integer overflow.

3. **Document TCB:** Clearly communicate to users that code extraction
   is part of the trusted base.