Compositional Assurance with the IRON COMPASS Framework: Integrating Formal Verification with Statistical Test and Evaluation for Mission-Critical AI Systems

Defense acquisition programs increasingly incorporate AI and machine learning components into mission-critical systems. This creates a T&E challenge: how to provide rigorous assurance for systems whose behavior emerges from learned parameters rather than explicit programming, and whose input spaces are effectively infinite (Director, Operational Test and Evaluation 2025). The challenge is acute for autonomous and semi-autonomous weapon systems, where DoD Directive 3000.09 (2023) requires verification and validation sufficient to provide confidence that systems perform as intended under operational conditions and resist unintended engagements. DoD Manual 5000.101 (2024) further prescribes operational test and evaluation (OT&E) and live-fire test and evaluation (LFT&E) requirements specifically for AI-enabled and autonomous systems, including treatment of operationally representative conditions such as inadvertent or malicious data poisoning and model hallucinations. Throughout this paper, “mission-critical” denotes systems whose failure may result in loss of life, compromise of national security information, or significant operational harm, consistent with the scope of DoDD 3000.09, DoDI 5000.98, and DoDM 5000.101.

Three established paradigms are available and none suffices alone. Statistical T&E characterizes behavior through designed experiments and confidence intervals (Freeman, Avery, and Johnson 2019), but no finite sample can guarantee that undesirable behaviors never occur (National Research Council 2012). Formal verification using Satisfiability Modulo Theories (SMT) solvers such as Z3 (de Moura and Bjørner 2008) and cvc5 (Barbosa et al. 2022) proves properties universally with respect to the encoded specification (Barrett and Tinelli 2018), with demonstrated deployment in safety-critical domains — Alt-Ergo was qualified for use in the DO-178C certification package of a commercial aircraft (Moy et al. 2013), and AWS has deployed formal verification across its cloud services (Cook 2018). Yet verification of arbitrary properties of large neural networks remains intractable, and some requirements resist formal specification. Large language models, which can translate natural-language requirements into formal logic, cannot reliably check themselves: hallucination is an innate limitation derivable from learning-theoretic and computability arguments (Xu, Jain, and Kankanhalli 2024; Banerjee, Agarwal, and Singla 2024), and the probability signal that would flag an error is the same signal that produced it.

Current practice treats these paradigms as separate concerns. The Defense Science Board has called for unified T&E approaches addressing software and AI complexity (Defense Science Board 2024), and current DoD guidance acknowledges the need but does not prescribe a methodology (DoD Instruction 5000.98 2024). IRON COMPASS — a codename in the defense naming tradition rather than an acronym — responds by partitioning AI requirements by verification tractability, binding each partition to the strongest feasible method, placing each tier at the right lifecycle phase, requiring drift monitoring after deployment, and combining the evidence into an integrated audit record.

1.1 Contribution and Relation to Prior Frameworks

The contribution is method-binding and evidence synthesis, not a new verification technique. SMT solvers, statistical T&E, drift detection, assurance-case argumentation (Bloomfield and Bishop 2017), runtime compliance checking (Amazon Web Services 2025; Bayless et al. 2025), and neurosymbolic validation of reasoning (Feng et al. 2025) are all mature. What IRON COMPASS adds over existing assurance-case and ML lifecycle frameworks is summarized in Table 1.

Table 1. IRON COMPASS compared with prior assurance frameworks.

Goal Structuring Notation and related assurance-case methods (Bloomfield and Bishop 2017) specify how evidence supports a claim but are method-agnostic; ML lifecycle frameworks (Chandrasekaran et al. 2024; Batarseh, Freeman, and Huang 2021) catalog available practices across the lifecycle but do not prescribe method selection as a function of property class. The NIST AI Risk Management Framework (Tabassi 2023) defines outcome-level risk-management functions (GOVERN, MAP, MEASURE, MANAGE) but is intentionally non-prescriptive about which verification or evaluation method to apply to which property. IRON COMPASS makes that binding explicit and adds a property-class to SMT-theory-fragment mapping, an operational classification procedure, required drift monitoring, and an independence discipline. The framework is proposed through a worked example and an executed reference instance (Section 5.5); empirical evaluation on operational systems is future work.

Four specific elements are novel rather than syntheses of prior work. First, the property-class to SMT-theory-fragment mapping in Section 3.1 is a new taxonomy from AI safety and policy-compliance property forms to specific SMT theories with runnable encoding sketches (a subset of which is executed in Section 5.5); individual encodings are standard but the mapping as a T&E methodology has not previously been published. Second, the four-tier compositional stack with tier-specific audit schema is novel in its integration: assurance-case frameworks specify argument structure without prescribing evidence types, and ML lifecycle frameworks catalog evidence without unifying it into a single schema. Third, required drift monitoring as a Tier 2 runtime obligation tied to a pre-deployment bound is a novel accreditation condition. Fourth, the explicit application of the legal evidence-independence criterion (Grimm, Grossman, and Cormack 2021) to compositional AI assurance, with the pre-deployment specification and the classifier oracle named as the residual coupling artifacts, is a novel framing. The remaining elements — SMT verification, statistical T&E, drift detection, assurance-case argumentation, neurosymbolic validation — are mature and cited as such.

IRON COMPASS partitions AI system requirements into four assurance tiers distinguished by the strength of evidence each supports. A visual summary of the tiers, their lifecycle placement, and the failure mode that justifies each one is provided as Supplemental Figure 1S at the end of this paper. Each tier specifies pre-deployment work, runtime work, and the evidence preserved for audit.

2.1 The Four Tiers

Tier 1 — Formally Verified. Properties proven to hold on every released output via SMT or equivalent formal methods. Evidence: independently checkable verification certificates.

Tier 2 — Statistically Bounded. Properties characterized with confidence intervals from designed experiments, plus post-deployment drift monitoring against the bounds established pre-deployment.

Tier 3 — Empirically Tested. Properties evaluated by independent subject-matter experts (SMEs) on representative scenarios using pre-registered rubrics. Evidence is observational and limited to tested cases.

Tier 4 — Documented Context with Monitoring Obligation. Properties accepted based on rationale, heritage, or operational constraint outside the system-under-test — network availability, vendor behavior, upstream data provenance — with an assumption register and a monitoring plan that triggers re-review when assumptions are violated. Tier 4 is not an assurance claim about the system; it is a disciplined record of what has been assumed and how those assumptions will be policed.

2.2 Why Four Tiers

The partition is not arbitrary. Each tier corresponds to a distinct epistemic commitment: universal proof with respect to a specification (Tier 1), probabilistic characterization with drift policing (Tier 2), structured human judgment (Tier 3), and audited assumption (Tier 4). Collapsing Tier 4 into Tier 3 would mask the distinction between properties of the system and properties of its environment; collapsing Tier 2 into Tier 1 would permit statistical claims to be read as guarantees; collapsing Tier 3 into Tier 2 would demand metrics where none reliably exist. The four-tier structure is the minimum partition that keeps each class of evidence honest about what it proves.

2.3 Operational Classification Procedure

A property is assigned to a tier by answering four ordered questions. The procedure produces a defensible tier assignment together with the reasoning trail required for audit. Latency thresholds and criticality judgments are program-specific and are to be stipulated pre-deployment. The procedure does not eliminate engineering judgment; it constrains and documents it. Latency thresholds in Q2 are stipulated at accreditation time based on the decision cycle the system supports, and SME-rubric judgments in Q4 must satisfy the independence requirements of Section 4. Where a single operational requirement combines elements of multiple tiers — for example, an output-content requirement combined with a performance requirement — the requirement is partitioned into its constituent properties, each classified separately. The decision procedure is summarized in Table 2.

Table 2. Classification decision procedure.

Because tier assignment determines the assurance method, the classification must be reproducible across analysts, and the four questions therefore carry anchored decision criteria rather than unaided judgment. Q1 is answered YES only when a type-correct encoding of the property exists in one of the theory fragments of Table 3 and returns correct verdicts on a small known-pass/known-fail probe set; inability to produce such an encoding after documented effort is a NO. Q2 is answered against measured per-output latency (median and p95) on representative outputs, compared to the budget stipulated at accreditation time — not against intuition about solver speed. Q3 requires that a metric definition, a sampling frame, and a target confidence level all be written down; if any of the three cannot be stated, the answer is NO. Q4 requires a pre-registered rubric and at least two independent SMEs; absent either, the property falls to Tier 4. To police residual judgment, IRON COMPASS requires dual classification: two analysts classify independently, disagreements are adjudicated with a documented rationale, and both the disagreement rate and the adjudication record are preserved in the audit record. Inter-rater characterization of the procedure across programs is future work.

Decomposition of compound requirements is likewise governed by explicit rules, applied before classification and recorded in the audit trail, because different analysts may otherwise partition the same operational requirement differently and arrive at different assurance strategies. A property is atomic when it concerns a single observable, yields a single pass/fail or scored verdict, and can be evidenced by a single method. Rule 1: split conjunctions over distinct observables (content and latency; format and accuracy) into separate properties. Rule 2: split elements with different verdict types — a checkable pattern or numeric bound is separated from a holistic judgment. Rule 3: after Rules 1 and 2, the holistic remainder is classified as a whole (typically Tier 3) rather than atomized further; over-decomposition of judgment properties manufactures pseudo-metrics. Applied to the worked example’s “response tone and operational fit,” Rule 2 first extracts the checkable advisory-prefix format requirement (Tier 1, Class A2), leaving tone appropriateness and operational fit as the holistic Tier 3 remainder evaluated by the Section 5.3 rubric. Two analysts may still decompose a novel requirement differently; the discipline the framework imposes is that the decomposition itself is an auditable, adjudicated artifact, so divergent decompositions are visible and resolvable rather than silent.

An SMT solver determines whether a logical formula combining Boolean operators with theory predicates is satisfiable; modern solvers couple a SAT engine with theory solvers for arithmetic, strings, arrays, and bit-vectors (Barrett and Tinelli 2018). For T&E, SMT is attractive for three reasons. First, the verdict is definitive with respect to the encoded formula. At runtime the formula is variable-free — the concrete output is bound before the query is issued — so the check reduces to evaluation and cannot return a wrong verdict for solver-completeness reasons. In pre-deployment use, where formulas contain free variables (the rule-set consistency proof of Section 4), UNSAT proves universal satisfaction over the inputs the formula describes; in fragments such as QF_SLIA this proof is subject to solver incompleteness — strings with length constraints are not decidable in general, so solvers are sound but may return unknown — and unknown is handled fail-closed. Either way, the claim is distinct from a claim about all outputs the model could ever generate. A Tier 1 claim in IRON COMPASS is therefore carefully bounded: every released output was checked, and the runtime checker — not the model — is the source of the guarantee. Second, modern solvers produce independently checkable proof objects. Third, latency is fast enough for per-output runtime use. In the executed reference instance of Section 5.5, the composed three-constraint check of Section 5.1 ran through Z3 4.16.0 on 400 synthetic outputs at a median of 3.0 ms per output (mean 3.0 ms, p95 = 4.2 ms, maximum 28.8 ms; single core of an Intel Xeon at 2.10 GHz), well within the interactive budgets of Table 2.

Alternative formal methods exist but are less well suited to Tier 1 content checking as defined here. Propositional SAT cannot express real-arithmetic thresholds, string patterns, or bit-vector fields without exponential bit-blasting. Abstract interpretation scales well but computes sound over-approximations that sacrifice the precision required for output-content decisions. Interactive theorem provers (Coq, Isabelle) achieve the strongest guarantees but require human proof effort incompatible with per-output runtime checking. Temporal model checkers target state-machine properties rather than single-output predicates. Neural-network verification tools such as Marabou 2.0 (Wu et al. 2024) are themselves SMT-based and extend the approach to model-internal properties; Liu et al. (2021) survey the broader neural-network verification landscape. SMT is therefore the best available match for the specific combination of requirements Tier 1 imposes: decidable content predicates, independently checkable proof objects, and sub-budget latency per output.

A fair question is what the SMT machinery buys at runtime, since a variable-free query reduces to evaluation and a conventional deterministic checker (regular-expression and length tests) returns the same verdicts roughly two orders of magnitude faster (Section 5.5). Three things. First, formalism identity: the artifact proved consistent and non-vacuous pre-deployment is byte-identical to the artifact executed at runtime, eliminating the translation gap between a verified specification and a hand-written checker that merely resembles it. Second, standard evidence: verdicts arrive as SMT-LIB queries with checkable solver artifacts in a vendor-neutral format, which is what the Tier 1 audit record preserves. Third, headroom: constraints that outgrow pure evaluation — arithmetic over extracted fields, cross-field consistency, bounded quantification — stay in the same formalism rather than forcing a checker rewrite. Where none of these matter for a given constraint, a deterministic checker validated against the SMT specification is an acceptable Tier 1 implementation; the specification, not the execution engine, is what the tier requires.

3.1 Property-Class to Theory-Fragment Mapping

AI safety and policy-compliance properties recur in a small set of classes, each matched to an SMT theory fragment. The mapping in Table 3 — expanded from the four classes of earlier versions of this framework to nine — is intended as a working taxonomy for T&E practitioners, not an exhaustive enumeration. Each class is accompanied by a sketch of its SMT-LIB encoding. Individual encodings are standard SMT; the classification as a methodology for AI T&E is the contribution.

Table 3. Property-class to SMT-theory-fragment mapping with encoding sketches.

Properties that do not fit a single class — for instance, temporal or multi-turn conversational properties that range over sequences of outputs — can often be decomposed into per-step constraints plus an auxiliary history predicate encoded via uninterpreted functions, or deferred to Tier 2 where their statistical behavior can be characterized. Properties that range over distributions rather than individual outputs (calibration, fairness metrics) are Tier 2 by construction. The taxonomy in Table 3 is intended to cover the properties most often encountered in policy-compliance and safety-constraint work and is extensible as additional property classes are encountered in practice.

3.2 Why LLM Self-Check Cannot Carry Tier 1

A natural question is whether an LLM can check its own outputs against formal specifications. It cannot carry a Tier 1 guarantee. Likelihood, attention weights, and decoding probabilities are optimized for plausibility under the model distribution, not for logical validity within a given context. Hallucinated outputs are therefore often high-likelihood outputs in the producing model’s own distribution — the probability signal that would flag an error is the same signal that produced it. Xu, Jain, and Kankanhalli (2024) show using learning-theoretic arguments that LLMs cannot learn all computable functions and will inevitably produce inconsistencies when deployed as general problem solvers. Banerjee, Agarwal, and Singla (2024) extend this analysis to every stage of the LLM pipeline.

The framework’s position is more precise than “no LLM, ever, at Tier 1.” The operative requirement is evidence independence: Tier 1 evidence must come from a source whose failure modes are uncorrelated with the system under test. An SMT solver provides such evidence because it does not share the generator’s training distribution or architectural biases. A separate LLM, used as a checker, does not automatically provide such evidence: training-data overlap, shared architectural priors, and correlated failure modes are the rule rather than the exception. Neurosymbolic approaches such as VeriCoT (Feng et al. 2025) are consistent with this position precisely because they use an LLM to translate reasoning into a form a symbolic checker can verify, rather than using the LLM itself as the final arbiter. In IRON COMPASS terms, the LLM is a translator; the symbolic checker is the Tier 1 evidence source. LLM-based judging without a symbolic backstop is classified at Tier 3, alongside human SME review — it is not excluded, but it is not Tier 1.

3.3 Adversarial Robustness of the Verification Layer

For defense T&E, the Tier 1 claim must be robust against adversarial inputs directed at the verification layer itself, not only the model. Three threats deserve explicit treatment. Specification gaming — outputs that satisfy the encoded constraint while violating its intent — is a specification-encoding risk mitigated by the pre-deployment encoding-validation requirement in Section 4 (domain-expert review, known-pass/known-fail test cases, and a standalone consistency proof of the rule set). Input crafting against the encoder — inputs exploiting Unicode, whitespace, or escape-character corner cases that cause UNSAT to be returned for the wrong reason — is mitigated by input canonicalization prior to encoding and fuzzing of the encoder as part of pre-deployment validation. Resource exhaustion — inputs crafted to push solver latency past the operational budget — is mitigated by a stipulated latency budget with a fail-closed policy for solver timeouts (an unresolved query blocks the output and logs the event rather than releasing it on timeout). These mitigations are not novel individually; their inclusion as Tier 1 preconditions is what IRON COMPASS specifies.

Each tier operates in specific phases of the AI system lifecycle. Tier 1 begins pre-deployment with constraint encoding and validation — review by domain experts against the natural-language source, testing against known-pass and known-fail cases, and rule-set consistency checking as a standalone solver query — then runs continuously at runtime on every generated output. Tier 2 establishes statistical bounds pre-deployment through designed experiments and continues post-deployment through drift monitoring against those bounds. Tier 3 conducts SME panel review pre-deployment; the evidence ships with the system but does not execute against live decisions. Tier 4 enumerates environmental assumptions pre-deployment and monitors for assumption violations at runtime.

4.1 Statistical Drift Monitoring

Pre-deployment Tier 2 bounds hold only if the operational input distribution continues to resemble the test distribution. Three statistical methods are standard for detecting drift. The Kolmogorov–Smirnov test compares empirical cumulative distributions of a continuous feature in reference and current data; rejection of the null of identical distributions signals drift. The chi-squared test gives an analogous check for categorical features. The Population Stability Index (PSI), developed in credit scoring and adopted widely for ML monitoring (Lin 2017; Yurdakul 2018), aggregates bin-wise log-frequency differences into a single score. PSI thresholds in industry practice — below 0.1 indicating no significant change, 0.1 to 0.25 warranting closer monitoring, 0.25 and above indicating likely need for recalibration — are conventions derived from operational experience rather than statistical theorems, and should be set pre-deployment based on the criticality of the downstream decision. PSI is univariate, bin-dependent, and known to be relatively insensitive to small or multivariate shifts; for programs requiring higher sensitivity, Jensen–Shannon divergence, Wasserstein distance, or kernel-based maximum mean discrepancy (MMD) provide alternatives with different sensitivity profiles. Metric choice is a program-specific tradeoff between sensitivity, interpretability, and computational cost; the framework does not prescribe a single metric but requires that the choice be declared pre-deployment and preserved in the audit record.

Drift monitoring under streaming data raises well-known statistical pitfalls that IRON COMPASS requires practitioners to address explicitly. Repeated application of a fixed-α hypothesis test across many windows inflates the family-wise false-positive rate; monitoring multiple features multiplies it further. The framework therefore distinguishes two distinct statistical activities: pre-deployment characterization, which uses stated α levels and reports confidence bounds as a claim about the test distribution; and runtime drift detection, which treats statistical tests as triggers for investigation rather than as hypothesis tests with stated type-I error. Where statistical guarantees are required on drift detection — for example, where drift detection feeds an automated re-accreditation trigger — sequential methods such as CUSUM or change-point detection are preferred over repeated fixed-window tests, and multiple-testing corrections (Bonferroni at minimum, hierarchical where appropriate) must be applied across the monitored feature set.

IRON COMPASS specifies drift monitoring as a Tier 2 runtime activity with three requirements: preserve the pre-deployment test distribution as the reference baseline; run drift tests continuously or at operationally appropriate intervals against thresholds set pre-deployment with documented multiple-testing policy; and flow findings into the audit record with decision logic connecting drift severity to investigation, re-test, or re-accreditation. A Tier 2 claim in IRON COMPASS is therefore compound: the measured statistic fell within the confidence bound declared pre-deployment at the stated α level on the pre-deployment test distribution, and continuous monitoring has not detected drift — against thresholds set with the declared multiple-testing policy — that would invalidate that bound in current operation.

4.2 The Audit-Record Schema

The audit record is the union of four tier-specific evidence streams preserved for the life of the system.

• Tier 1. Constraint specifications in SMT-LIB, encoding-validation evidence (domain-expert review record, known-pass/known-fail test corpus, rule-set consistency proof), input-canonicalization policy, solver timeout policy, and a proof certificate for every verified runtime output.
• Tier 2. Test design, sampled inputs and outputs, confidence bounds with reproducibility seeds, declared multiple-testing policy, and the continuous drift time-series with threshold crossings logged.
• Tier 3. Vignettes, pre-registered rubrics, reviewer ratings, qualitative comments, and reviewer identities preserved for challenge; review protocol including inter-rater agreement statistics.
• Tier 4. The assumption register with rationale, the monitoring plan, and the log of any assumption violations observed during operation.

The record supports three audit uses: reconstructing the evidence basis behind any questioned decision, detecting distributional shifts before they manifest as failures, and providing the structured evidence package for re-accreditation without redundant testing.

The audit-record schema maps onto the Test and Evaluation Master Plan (TEMP) structure specified in DoD Manual 5000.100 (2024), issued under DoD Instruction 5000.98 (2024), and satisfies the AI-specific evidence requirements prescribed in DoD Manual 5000.101 (2024). Tier 1 evidence supplies the TEMP’s verification evidence for requirements that must hold under all operational conditions. Tier 2 evidence populates the TEMP’s OT&E data requirements and the AI-enabled-system evaluation inputs called for in DoDM 5000.101. Tier 3 evidence supports operational assessment and suitability evaluation. Tier 4 evidence populates the assumptions, constraints, and limitations sections. The framework does not prescribe a new TEMP structure; it organizes evidence so that accreditation artifacts can be assembled from tier-specific stores without rederivation.

Two specific DoDI 5000.98 artifacts are worth naming. The Integrated Decision Support Key (IDSK) links operational performance metrics and test data across acquisition decisions; Tier 1 proof certificates and Tier 2 confidence bounds supply this linkage directly, and Tier 2 drift findings update IDSK performance characterizations as operational data accumulates. The Mission-Based Risk Assessment (MBRA) characterizes system behavior under adversarial and degraded conditions; Tier 1 adversarial-robustness evidence (Section 3.3) and Tier 2 drift monitoring update the MBRA across the lifecycle. The audit-record schema is designed so that populating these artifacts does not require a separate evidence-collection activity.

4.3 Evidence Independence

The compositional argument depends on the claim that the four tiers fail independently. This claim deserves defense rather than assertion. The tiers share two residual couplings that deserve naming. The first is the pre-deployment specification of the property to be verified. A defective specification corrupts Tier 1 (the encoded constraint is wrong), Tier 2 (the metric may be measuring the wrong thing), and potentially Tier 3 (the rubric may target the wrong behavior). This is the single most important residual correlation in the framework, and it is mitigated — not eliminated — by the Tier 1 pre-deployment encoding-validation activity and by the rubric-review activity that Tier 3 requires.

The second coupling is the classifier oracle. Where a Tier 1 constraint rests on a classifier score — the dominant architecture for operational LLM constraints, as Section 6 details — the same classifier is a common failure source for the Tier 1 check that consumes its score and for the Tier 2 characterization of the system, and the framework’s own mitigation (characterizing the oracle under Tier 2) makes that Tier 1 evidence conditional on Tier 2 evidence. Oracle-backed constraints therefore do not participate in the independence argument as unconditional Tier 1 evidence; they participate as Tier-1-conditional-on-Tier-2 evidence and are recorded as such in the audit record.

Conditional on a correct specification, and restricted to Tier 1 constraints whose semantics are solver-internal (no external oracle; Section 6), the residual failure modes of the tiers are substantially independent. Tier 1 failures arise from solver bugs, encoder bugs, or specification-gaming that the encoding did not anticipate. Tier 2 failures arise from sampling bias, drift, or metric choice. Tier 3 failures arise from rater bias, rubric ambiguity, or insufficient scenario coverage. Tier 4 failures arise from violated environmental assumptions. These failure modes do not share a common mechanism after the specification is fixed, which is what the compositional argument requires. The legal-admissibility literature treats evidence independence as a reliability criterion (Grimm, Grossman, and Cormack 2021); IRON COMPASS adopts the same discipline and makes the residual coupling through the specification an auditable artifact rather than a hidden dependency. The independence claim here is a structural argument about failure-mode mechanisms, not a formal probabilistic proof; empirical characterization of residual correlations between tiers is future work.

This argument establishes methodological independence — the tiers’ technical failure mechanisms are distinct. It does not by itself establish operational independence. Real programs can re-couple the tiers through shared resources: the same analysts writing the Tier 1 encoding and the Tier 3 rubric; a common dataset used for Tier 2 characterization and Tier 3 vignette construction; shared tooling or pipelines whose defects propagate into multiple evidence streams; and common governance assumptions that shape what every tier looks for. IRON COMPASS therefore requires that the accreditation case declare, per tier, the personnel, datasets, tools, and governance processes on which its evidence depends, and that overlaps be either removed (separate teams, disjoint datasets — the Section 5.2 requirement that the OTA withhold the Tier 2 test set from developers and rubric authors is one instance) or recorded as declared couplings that weaken the compositional claim. The compositional argument holds to the extent that both the methodological and the declared operational couplings are absent or characterized; it is not an unconditional property of the four-tier structure.

Note on scope. Sections 5.1–5.4 specify how IRON COMPASS would be applied to a representative AI system; Section 5.5 then executes the Tier 1 and Tier 2 evidence paths of that specification on synthetic data, with real solver runs and measured latencies. No study of an operational system was conducted; validation on operational systems is future work.

Consider a large language model deployed as a logistics planning decision-support tool. The system accepts natural-language queries from a human planner and returns recommendations; the planner retains decision authority (consistent with DoD Instruction 5000.98 2024). Applying the classification procedure of Section 2.3 yields the assignments in Table 4.

Table 4. Tier assignments for the logistics decision-support example.

5.1 Tier 1 Encoding Sketch

The unauthorized-command constraint is expressed as a Class A1 property in QF_SLIA. Sketch SMT-LIB:

(set-logic QF_SLIA)

(declare-const output String)

(assert (not (str.contains output “shutdown”)))

(assert (not (str.contains output “launch_authorize”)))

(check-sat)

The assertions above state the composed property P in specification form; the same P is the object of the pre-deployment consistency proof. At runtime the generated output is bound to the constant and the solver is queried on the negation of the composed property (assert (not P)): UNSAT certifies that no violation exists and releases the output; SAT yields a violating witness, blocks the output, and logs the violation. Length and PII constraints are composed into the same query through additional asserts. Pre-deployment encoding validation consists of domain-expert review of the constraint list, a test corpus of 200 known-pass and 200 known-fail cases sized to exercise all cataloged restricted-command patterns plus their documented evasion variants, and a standalone consistency proof confirming the rule set admits at least one satisfying assignment.

5.2 Tier 2 Bounds and Drift Policy

Response accuracy is characterized on a stratified sample of 2,000 queries drawn across four query-type strata (500 per stratum), sized to yield 95% Wilson-score confidence intervals no wider than approximately ±3.5 percentage points per stratum and ±1.8 points on the aggregate estimate at expected accuracy of 0.80 (per-stratum ±3.0 points would require roughly 700 queries per stratum). The test dataset is withheld by the operational test agency (OTA) and is not available to system developers during training or to reviewers during Tier 3 rubric construction, consistent with DoDM 5000.101 (2024). Per-stratum confidence intervals are computed using the Wilson score method for binomial proportions; Clopper–Pearson intervals may be substituted where conservatism is preferred. p95 latency is characterized with a KS-based drift monitor on the latency distribution. PSI is computed daily on query-type categories, query length, and predicted-accuracy deciles; thresholds follow the conventional 0.1 / 0.25 bands with a Bonferroni correction across the three monitored features. A PSI breach on any feature triggers an investigation workflow logged to the audit record. The distinction in Section 4.1 between pre-deployment characterization (stated α, fixed sample, reported as a confidence bound) and runtime drift detection (investigation trigger, not a hypothesis test with stated type-I error rate) is preserved: Tier 2 evidence is reported with explicit type-I error rate pre-deployment and as trigger-based findings post-deployment.

5.3 Tier 3 Rubric Sketch

Usability is rated by three independent SMEs on a pre-registered 5-point rubric covering tone appropriateness (5 = appropriate for operational planning context; 1 = unsuitable), format fit (5 = conforms to planner workflow; 1 = requires rework), and operational relevance (5 = actionable; 1 = not actionable). Inter-rater agreement is reported via Krippendorff’s alpha; for mission-critical T&E, the threshold is set at α ≥ 0.80, consistent with Krippendorff’s recommendation for reliable conclusions (values in the 0.67–0.80 range support only tentative conclusions and are inappropriate for accreditation evidence). Ratings below threshold trigger rubric review. Reviewer identities and all comments are preserved.

5.4 Tier 4 Assumption Register

Infrastructure availability is entered in the assumption register at ≥99.9% with reference to the vendor SLA; violations (vendor-reported outages, dependency failures, data-provenance breaches) trigger an assumption re-review and potential re-accreditation of the affected Tier 2 bounds.

Sections 5.1–5.4 establish that the framework can be specified end-to-end, with concrete operationalization at each tier. Specification is not application: the executed reference instance that follows demonstrates that the Tier 1 and Tier 2 evidence paths of this specification run as described, with measured latencies and computed bounds. Neither establishes operational performance; that is future work.

5.5 Executed Reference Instance

To move the worked example from specification to execution, the Tier 1 and Tier 2 evidence paths of Sections 5.1–5.2 were implemented and run. All data are synthetic and labeled as such: the instance demonstrates the runtime mechanics and measures their cost; it does not characterize any operational system. The script, random seed, and raw results are provided as Supplemental Material 2S.

Tier 1. The composed Section 5.1 property — no restricted command (“shutdown”, “launch_authorize”), no SSN-format pattern (Class A1, encoded via str.in_re), and output length ≤ 4,096 (Class E1) — was executed in QF_SLIA through Z3 4.16.0 (Python bindings; single core of an Intel Xeon at 2.10 GHz; Ubuntu 24.04). The pre-deployment validation corpus of Section 5.1 was instantiated at its stated size: 200 known-pass and 200 known-fail synthetic logistics outputs (70 restricted-command, 70 PII-pattern, 60 over-length). Each output was checked with a fresh per-output query asserting the negation of the composed property. Table 5 reports the results.

Table 5. Executed reference instance — measured results (synthetic data; Z3 4.16.0; single 2.10 GHz core; seed 20260707).

Tier 2. The statistical path was executed on seeded synthetic data mirroring the Section 5.2 design: four strata of 500 Bernoulli-drawn outcomes with per-stratum accuracies between 0.77 and 0.84. Wilson 95% intervals came in at half-widths of 3.2–3.7 percentage points per stratum and ±1.7 points on the aggregate — the execution that surfaced the sample-size correction now reflected in Section 5.2. The PSI drift monitor was run over 30 simulated days of query-type category frequencies (n = 250 per day) with a distribution shift injected at day 21; PSI remained below 0.04 across the 20 pre-shift days and crossed both the 0.10 and 0.25 bands on day 21, triggering the investigation workflow on the first post-shift day.

The instance substantiates three specific claims and no more. First, the Q2 latency premise is measured rather than asserted: the per-output check runs at single-digit milliseconds against a 50 ms interactive budget on commodity hardware, with correct verdicts on all 400 known cases. Second, the fail-closed policy of Section 3.3 is exercised rather than hypothetical: under deliberately tight budgets the solver returned unknown and the checker blocked and logged. Third, the Q1 anchor of Section 2.3 — a type-correct encoding returning correct verdicts on known-pass/known-fail probes — is demonstrated concretely. What the instance does not show is equally specific: nothing here measures an operational model, an operational input distribution, or classifier-oracle behavior. Those remain future work, and the synthetic-data labels in Supplemental Material 2S are the audit trail for that boundary.

The four tiers form a verification stack in which each layer performs a distinct role and exhibits a distinct failure mode. An LLM used to verify an LLM shares training distribution and architectural biases, so a hallucinated output may be judged plausible by the checker. An SMT solver used without pre-deployment encoding validation can return UNSAT on a formula that does not capture the intended property. A statistical test without drift monitoring or multiple-testing discipline cannot reliably detect post-deployment distribution shift. A human review panel without structured rubrics and independent reviewers is subject to bias and coordinated error. The compositional arrangement, together with the independence discipline of Section 4.3, is the property that makes the overall assurance argument defensible against any single-point failure.

Several limitations bound the framework’s applicability. Vague requirements must be operationalized into verifiable constraints; autoformalization (Bayless et al. 2025) reduces but does not eliminate this burden. Verifying arbitrary properties of arbitrary neural networks remains intractable for large networks and complex properties. Most importantly, a per-output SMT check proves the constraint for each checked output, not for all outputs the model could generate without being checked — the Tier 1 claim is that every output released was verified, and the runtime checker is the source of the guarantee, not the model. The residual coupling of the tiers through the pre-deployment specification is the single strongest residual risk to the independence argument and deserves explicit treatment in any program-specific accreditation case. Empirical validation on operational systems is future work.

A further limitation deserves separate treatment: the classifier-oracle problem. Many practical constraints — particularly for operational LLM deployments — rely on classifier outputs that the SMT solver treats as given: a toxicity score (Table 3, Class B1), a PII-pattern detector, a prompt-injection classifier, a content-moderation classifier, a data-provenance classifier. In operational AI T&E this is the dominant architecture rather than an edge case. The SMT layer proves that the output satisfies the constraint conditional on the classifier’s score, but the classifier is itself a statistical model with its own error rate and drift characteristics. This leaks Tier 2 risk into the Tier 1 evidence stream. The framework’s partial mitigation is to require that classifier oracles used in Tier 1 constraints be separately characterized under Tier 2 — with confidence bounds on classifier accuracy and drift monitoring on classifier-input distributions — and that the composed claim be recorded in the audit record as conditional on the classifier’s characterized performance. A full solution requires classifier-level formal verification or conservative classifier bounds, neither of which is currently tractable at scale. Practitioners should treat Tier 1 constraints built on classifier oracles as Tier 1 with respect to the constraint logic but Tier 2 with respect to the oracle, and surface this distinction explicitly in the accreditation package. The IRON COMPASS audit-record schema accommodates this by recording oracle identities, versions, and characterized performance alongside the Tier 1 proof certificates that depend on them. A distinction within the oracle category is worth preserving: classifier oracles are statistical objects and take the Tier 2 treatment above, whereas deterministic oracles — the hash implementation behind a Class D1 integrity check, the authorization table behind Classes C1–C2 — are not characterized by confidence bounds; they sit in the trusted computing base and are assured by conventional software verification, with identity and version recorded in the audit record. Table 3 flags both kinds as oracle-conditional.

IRON COMPASS is a proposed compositional assurance methodology for mission-critical AI systems, integrating formal verification, statistical T&E with drift monitoring, empirical testing, and documented assumption. Its contribution is method-binding and evidence synthesis: it tells practitioners how to classify properties, which verification method to apply at each tier, how to place each tier at the right lifecycle phase, how to defend the independence of the resulting evidence streams, and how to preserve the evidence in an integrated audit record. The worked example and executed reference instance show that the framework can be specified end-to-end and that its Tier 1 runtime path meets interactive latency budgets on commodity hardware; validation across programs, analysts, and operational systems is the necessary next step. As AI systems assume increasingly critical defense roles, the demand for rigorous assurance will intensify. The compositional structure — not any single layer — is what carries the argument.

Amazon Web Services. 2025. “Minimize AI Hallucinations and Deliver up to 99% Verification Accuracy with Automated Reasoning Checks: Now Available.” AWS News Blog, August 15, 2025.

Banerjee, Sourav, Ayushi Agarwal, and Saloni Singla. 2024. “LLMs Will Always Hallucinate, and We Need to Live With This.” arXiv preprint arXiv:2409.05746.

Barbosa, Haniel, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, et al. 2022. “cvc5: A Versatile and Industrial-Strength SMT Solver.” In Tools and Algorithms for the Construction and Analysis of Systems, 415–442. LNCS 13243. Cham: Springer.

Barrett, Clark, and Cesare Tinelli. 2018. “Satisfiability Modulo Theories.” In Handbook of Model Checking, edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, 305–343. Cham: Springer.

Batarseh, Feras A., Laura Freeman, and Chih-Hao Huang. 2021. “A Survey on Artificial Intelligence Assurance.” Journal of Big Data 8 (1): 60.

Bayless, Sam, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, et al. 2025. “A Neurosymbolic Approach to Natural Language Formalization and Verification.” arXiv preprint arXiv:2511.09008.

Bloomfield, Robin, and Peter Bishop. 2017. “Safety and Assurance Cases: Past, Present and Possible Future — An Adelard Perspective.” In Making Systems Safer: Proceedings of the Eighteenth Safety-Critical Systems Symposium, 51–67. London: Springer.

Chandrasekaran, Jaganmohan, Tyler Cody, Niall McCarthy, Erin Lanus, Laura Freeman, and Kathy Alexander. 2024. “Testing Machine Learning: Best Practices for the Life Cycle.” Naval Engineers Journal 136 (1–2): 249–263.

Cook, Byron. 2018. “Formal Reasoning About the Security of Amazon Web Services.” In Computer Aided Verification (CAV 2018), 38–47. LNCS 10981. Cham: Springer.

Defense Science Board. 2024. Report of the Defense Science Board on Test & Evaluation. August 2024. Washington, D.C.: Office of the Under Secretary of Defense for Research and Engineering.

de Moura, Leonardo, and Nikolaj Bjørner. 2008. “Z3: An Efficient SMT Solver.” In Tools and Algorithms for the Construction and Analysis of Systems, 337–340. LNCS 4963. Berlin: Springer.

Director, Operational Test and Evaluation. 2025. FY2024 Annual Report. Washington, D.C.: Office of the Secretary of Defense, January 2025.

DoD Directive 3000.09. 2023. Autonomy in Weapon Systems. Office of the Under Secretary of Defense for Policy. January 25, 2023.

DoD Instruction 5000.98. 2024. Operational Test and Evaluation and Live Fire Test and Evaluation. Office of the Under Secretary of Defense for Acquisition and Sustainment. December 9, 2024.

DoD Manual 5000.100. 2024. Test and Evaluation Master Plans and Test and Evaluation Strategies. Office of the Director of Operational Test and Evaluation. December 9, 2024.

DoD Manual 5000.101. 2024. Operational Test and Evaluation and Live Fire Test and Evaluation of Artificial Intelligence-Enabled and Autonomous Systems. Office of the Director of Operational Test and Evaluation. December 9, 2024.

Feng, Yu, Nathaniel Weir, Kaj Bostrom, Sam Bayless, Darion Cassel, Sapana Chaudhary, Benjamin Kiesl-Reiter, and Huzefa Rangwala. 2025. “VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks.” arXiv preprint arXiv:2511.04662.

Freeman, Laura J., Kenneth Avery, and Thomas Johnson. 2019. “Designing Experiments for Model Validation — The Foundations for Uncertainty Quantification.” The ITEA Journal of Test and Evaluation 40 (1): 23–31.

Grimm, Paul W., Maura R. Grossman, and Gordon V. Cormack. 2021. “Artificial Intelligence as Evidence.” Northwestern Journal of Technology and Intellectual Property 19 (1): 9–106.

Lin, An Zheng. 2017. “Examining Distributional Shifts by Using Population Stability Index (PSI) for Model Validation and Diagnosis.” In Proceedings of the Western Users of SAS Software Conference, September 20–22, 2017. Long Beach, CA.

Liu, Changliu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J. Kochenderfer. 2021. “Algorithms for Verifying Deep Neural Networks.” Foundations and Trends in Optimization 4 (3–4): 244–404.

Moy, Yannick, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, and Benjamin Monate. 2013. “Testing or Formal Verification: DO-178C Alternatives and Industrial Experience.” IEEE Software 30 (3): 50–57.

National Research Council. 2012. Assessing the Reliability of Complex Models. Washington, D.C.: National Academies Press.

Tabassi, Elham. 2023. Artificial Intelligence Risk Management Framework (AI RMF 1.0). NIST AI 100-1. Gaithersburg, MD: National Institute of Standards and Technology. https://doi.org/10.6028/NIST.AI.100-1.

Wu, Haoze, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, et al. 2024. “Marabou 2.0: A Versatile Formal Analyzer of Neural Networks.” In Computer Aided Verification (CAV 2024), 249–264. LNCS 14682. Cham: Springer.

Xu, Ziwei, Sanjay Jain, and Mohan Kankanhalli. 2024. “Hallucination is Inevitable: An Innate Limitation of Large Language Models.” arXiv preprint arXiv:2401.11817.

Yurdakul, Bilal. 2018. “Statistical Properties of Population Stability Index.” Ph.D. dissertation, Western Michigan University.

Figure 1S. IRON COMPASS — Compositional Assurance for Mission-Critical AI. Four tiers of evidence, placed across the AI system lifecycle, combine into one audit record for the decision-maker. Each tier specifies pre-deployment work, runtime work, and the evidence preserved for audit. The bottom panel summarizes each layer’s failure mode, explaining why no single layer carries the assurance argument alone.