Individual skill

verification-boundary-reporter

Analyze formal verification artifacts (Isabelle, Coq, Dafny, etc.) and produce structured reports identifying the precise boundary between verified, assumed, and unverified components. Use when assessing verification coverage, understanding trust boundaries, auditing formal proofs, or documenting verification scope. Reports explicitly list verified code, assumptions, axioms, trusted computing base, and unverified components. Conservative and explicit about verification status without attempting to repair or mask gaps.

skills/verification-boundary-reporter/SKILL.md

Read pinned source

Source commit 4f38503747e0617504bce5329283ef837d375c09

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: No
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Not checked yet
Last checked: Nov 6, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 260
Repository last updated: Aug 21, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

claude-skills Repository topic
metaprogramming Repository topic
software-development Repository topic
software-engineering Repository topic
claude Repository topic
claude-code Repository topic
engineering Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 13,101 bytes
references/boundary_patterns.mddoc · 10,830 bytes
references/coq_analysis.mddoc · 10,909 bytes
references/dafny_analysis.mddoc · 10,825 bytes
references/isabelle_analysis.mddoc · 9,795 bytes

Read excerpt


# 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