Specification: Structural Assurability Pilot

Purpose

Investigate the applicability and limitations of Structural Assurability when evaluating concrete assurance claims and external evaluation frameworks.

The pilot examines whether claim-relative analysis can identify important distinctions among available observations, evidentiary capabilities, evaluator constraints, trust assumptions, and claim resolution.

The pilot may produce constructive examples, counterexamples, research findings, proposed formal extensions, or recommendations for external evaluation frameworks.

No particular outcome is presumed.

Initial Study

The initial study examines NIST's TEVV-Athlon framework.

Previously developed mapping work will be preserved and examined against the current Structural Assurability theory.

The initial questions concern:

• Explicit identification of evaluative claims.
• Relationships between claims and required evidence.
• Evidence accessible to a specified evaluator.
• Observation and instrumentation limitations.
• Assumptions about evidence integrity, provenance, and trust.
• Conditions under which available evidence cannot resolve a claim.

A public comment may be developed if the analysis identifies a specific, defensible issue and a useful proposed clarification.

Submitting a public comment is not a required research outcome.

Research Method

Each investigation should:

1. Identify the external source and preserve its provenance.
2. Identify the assurance claim or evaluation question.
3. Record the relevant observations and evaluator conditions.
4. Identify the assumptions on which the evaluation depends.
5. Map the question to applicable formal definitions and results.
6. Distinguish source statements from researcher interpretation.
7. Record counterexamples, limitations, or unresolved obligations.
8. Determine whether further analysis is justified.

Where executable experiments are useful, they must specify their admissible worlds, claims, observation channels, and assumptions.

Experimental outcomes must remain separate from formally proved results and empirical observations of operational systems.

Mapping Records

A mapping record should identify:

• A stable record identifier.
• Its source document, version, and location.
• The relevant source statement or evaluation requirement.
• The assurance claim or evaluation question.
• Relevant observations and evidence.
• Evaluator access and resource conditions.
• Applicable integrity, provenance, and trust assumptions.
• Related formal definitions or theorems.
• Any identified uncertainty.
• Supporting experiments or counterexamples, where available.
• The resulting finding or outstanding research question.

Research Boundaries

The Lean theory is authoritative for formal definitions and theorems.

The pilot does not establish the safety, trustworthiness, or adequacy of any evaluated system.

Finite-model experiments establish results only for their specified models and assumptions.

A structural-property difference does not independently establish a difference in evidentiary capabilities or claim resolution.

This repository does not modify the formal theory to accommodate an external framework or treat exploratory examples as formal proofs.

Outputs

The repository maintains:

• Source-grounded mappings of external evaluation frameworks.
• Explicit research questions.
• Reproducible experiments where needed.
• Findings, counterexamples, and unresolved questions.
• Documentation linking results to the formal theory.

Additional external frameworks or assurance cases may be added as independent studies.