75 Safety Cases and Structured Assurance

75.1 Chapter status

Field	Value
Chapter ID	`safety-cases-and-structured-assurance`
Part	Part IV - Evidence, Implementation, and the Living Book
Status	conceptual
Last updated	2026-07-15
Primary source records	`ext_gsn_community_standard_2011`, `ext_evaluations_safety_cases_scheming_2024`, `ext_aisi_safety_cases_2024`, `benchmaxxing`
Claim label	Design rationale
Evidence level	argument
Source loading state	source notes: `ext_gsn_community_standard_2011`, `ext_evaluations_safety_cases_scheming_2024`, `ext_aisi_safety_cases_2024`, `benchmaxxing`; raw cache: `benchmaxxing`
Test state	Eight finite record routes and an eight-case synthetic, digest-bound compiler bridge are implemented. No real assurance case, countercase search, reviewer workflow, acceptance decision, or release process has run.

75.2 Drafting guardrail

An assurance case is an argument map, not a safety certificate. This layer compiles bounded references from existing claim, evidence, evaluation, threshold, safeguard, readiness, provenance, and residual records so a reviewer can see what a proposed conclusion depends on and what might defeat it. It does not establish that the references are adequate, that the threat model is correct, that a control works, that a system is safe, or that anyone may deploy.

75.3 Human Reading Path

Concrete lens. The connected-graph baseline treats compilation as acceptance. The assurance packet separates compilation, challenge, review, and decision.

Complex systems can accumulate evidence far faster than they accumulate understanding. There may be test results, model cards, policy documents, proof files, incident notes, and approval records, yet no clear answer to a simple question: what is the argument for allowing this particular system to do this particular thing in this particular setting? A safety case makes that question visible instead of answering it with a folder full of artifacts.

The case links a claim to its reasons, evidence, assumptions, and conditions. It also records the reasons the claim may fail: an untested threat, a stale evaluation, a disputed inference, or a safeguard whose effectiveness has not been verified. These are not embarrassing footnotes. They determine whether a decision should proceed, narrow its scope, or wait for more work.

What remains is an argument that can be inspected and revised. It is not a mathematical proof of safety or a substitute for judgment. Its value lies in making disagreement, missing evidence, and residual risk impossible to hide inside an impressive-looking release decision.

75.4 Problem

The ASI Stack already produces many artifacts that matter to a high-consequence decision: a claim ledger, source notes, proof envelopes, evaluation records, threshold commitments, safeguard evidence, readiness gates, authority records, and residual escrow. Each has a local owner. A reviewer deciding whether a specific release path is justified still needs to understand how these pieces relate. Which risk is being addressed? Which claim is actually supported by a benchmark? Which safeguard is required? Which assumption makes the inference valid? Which failed evaluation or dissenting view would change the decision?

Without a compilation layer, the answer can become a narrative assembled at the end of the process. Narratives hide gaps well. A dashboard can show many green statuses while a critical hazard is outside the evaluation envelope. A report can cite a proof that establishes only record routing, not system behavior. A threshold non-crossing can be read as a safety result even though it says nothing about a different threat model. The missing capability is not documents; it is missing explicit relationships among documents.

Structured assurance turns those relationships into a reviewable object. It does not aim to make uncertainty disappear. It aims to identify the exact assumptions, countercases, evidence properties, and decision boundaries that would have to hold for a bounded conclusion to be defensible.

75.5 Why existing approaches are insufficient

Goal Structuring Notation provides a useful structural comparator: claims, strategies, evidence, context, assumptions, and justifications can be recorded as explicit relationships. The standard also states the key limitation: such a graph documents an asserted argument and does not establish its truth. An assurance case can therefore be well structured while its evidence is stale, its inference is invalid, its hazards are incomplete, or its decision owner is not authorized.

AI safety-case work supplies equally important limits. The evaluations-based scheming paper separates inability, harm, control, and alignment arguments, each with different evidence needs and unresolved assumptions. AISI’s safety case work emphasizes positive support, countercase searches, disagreement, and scientific uncertainty. These sources describe methodology and open problems, not a reusable safety conclusion. They show why a single template or confidence score cannot turn frontier-AI uncertainty into an operational all-clear.

Existing ASI Stack layers own inputs but not compilation. Evidence States owns support-state changes; Benchmark Ratchets owns quality of measurement pressure; Adversarial Evaluation owns the integrity of an observation; Capability Thresholds owns a predeclared response; Readiness owns admission; Artifact Graphs owns provenance; Security Kernel and Runtime Adapters own controls and authority. A safety case must reference these owners without swallowing them. Otherwise it becomes a second, less auditable ledger or a misleading layer of approval over the real decision process.

75.5.1 Strongest-neighbor comparison

The design delta is easiest to see by comparing ownership rather than by claiming a new notation. GSN supplies a vocabulary for argument structure. Evaluations-based safety-case work supplies risk-specific argument families and their empirical dependencies. AISI’s methodology supplies the obligation to search for counterevidence and preserve scientific uncertainty. The ASI Stack contribution proposed here is narrower: compile already governed records into a dependency-aware case, preserve the owners of those records, and make an unresolved dependency change the route of an affected release without allowing the compiler to approve it.

Comparator	Strong capability	Residual boundary	ASI Stack design delta
GSN Community Standard	Explicit goals, strategies, solutions, context, assumptions, and justifications.	A well-formed graph documents an asserted argument; it does not validate the argument or evidence.	Bind graph nodes to versioned claim and artifact identities, retain prior versions, and route stale or unresolved dependencies to their owning workflow.
Evaluations-based safety cases for scheming	Separates incapability, harm, control, and alignment arguments and exposes their different assumptions.	The framework does not supply missing empirical evidence or make evaluation reliability automatic.	Represent the selected argument family and evaluation envelope as case scope, not as a generic confidence score, and reject evidence reuse when that scope changes.
AISI safety-case methodology	Treats countercases, negative evidence, uncertainty, and disagreement as first-class.	Countercase quality and reviewer independence remain substantive empirical questions.	Require recorded countercase review, independent review, residual ownership, and non-claim boundaries before a case can reach readiness review.
ASI Stack evidence, threshold, readiness, and provenance layers	Own support movement, measurement pressure, precommitments, admission, custody, and replay.	Separate records do not by themselves express the whole argument for a bounded decision.	Compile references without duplicating ownership; a case status can block or request review but cannot promote evidence, waive a threshold, admit a system, or authorize an action.

This is not a claim that record compilation is stronger than substantive safety analysis. It is a claim about control-plane integrity. The useful question is whether a case can remain synchronized with the ledgers that determine its meaning, reveal when a dependency changes, and force an explicit response. A compiler that does those things can reduce argument drift even when every underlying scientific uncertainty remains.

75.6 Core Claim

[safety-cases-and-structured-assurance.core, label: Design rationale, support: argument] Safety Cases and Structured Assurance owns a deployment-context-, hazard-, claim-, strategy-, evidence-, assumption-, defeater-, safeguard-, threshold-, readiness-, authority-, release-path-, residual-, version-, and time-specific Assurance Argument Compilation Packet: it compiles exact governed references and bounded support or challenge relations, preserves alternatives, dissent, staleness, countercases, conflicts, overrides, costs, lineage, and downstream invalidation, and routes only a scoped case status to existing decision owners; a connected, rendered, notation-conformant, reviewed, accepted, or synthetically complete case alone establishes neither hazard completeness, evidence adequacy, argument validity, reviewer independence, control effectiveness, risk, safety, readiness, release authority, deployment, support, transfer, nor SOTA.

Reader claim. A safety case is a structured argument and challenge surface, not a certificate that the system is safe or permission to deploy it.

Operational rule. Bind each claim to exact deployment context, evidence version, assumptions, countercases, defeaters, safeguards, thresholds, reviewers, and residual owners. Stale evidence or an unresolved defeater blocks only the affected route and can advance at most to readiness review, never directly to release.

75.7 Mechanism

75.7.1 Eighteen-stage assurance lifecycle

The full lifecycle freezes the case boundary; compiles typed nodes; gives every edge an explicit bounded meaning; binds exact evidence identity and scope; records assumptions and justifications; maps hazards and the outside envelope; preserves defeaters, countercases, dissent, and unknowns; graphs reviewer dependencies and conflicts; binds acceptance criteria and residual custody; checks source-ledger freshness; separates structural, semantic, empirical, control, acceptance, readiness, and release states; keeps compile, challenge, review, accept, decide, override, release, revoke, and retire distinct; versions and invalidates descendants; preserves incompatible argument families; governs node-level disclosure; emits routing rather than authority; and measures case quality, disagreement, delay, burden, cost, residual age, and retirement.

The first object is a case boundary, written before an argument is assembled. It names the system and version, deployment context, top claim, threat and hazard model, affected release path, decision owner, acceptance criterion, review deadline, and case version. A top claim such as “safe” is unusable on its own. A bounded claim might concern a named system, a named access mode, a named harm model, and a named operating period. The boundary prevents a case prepared for one evaluation setting from being silently reused for another.

The second object is a typed argument graph. Each claim records its scope and support state. Each strategy says how a higher claim is decomposed. Each evidence reference points to an artifact owned elsewhere and identifies the property it is asserted to support. Context, assumptions, and justifications make the interpretation visible. A case does not copy a benchmark report, proof file, or policy decision into a prettier document. It records the exact relationship claimed between that artifact and a particular statement.

The third object is a defeater and countercase ledger attached to the graph. An unresolved counterexample, stale evaluation, missing threat-model review, contradictory evidence, unverified safeguard, or missing residual owner is a node with a route, not a prose caveat that a report generator can omit. A countercase search also records its scope and reviewer conditions, because a failed search is only informative when its ability to find a problem is itself open to review.

The final object is a decision boundary. Compilation may produce a draft case, a case requiring repair, a case requiring accountable review, a case with an affected release blocked, or a bounded input to the existing readiness gate. It never produces release authority. Acceptance and release remain separate records with their own owners, and a case revision is a reason to re-review the affected path rather than a way to overwrite prior uncertainty.

75.7.2 Case lifecycle and identity

A case begins as a draft with a stable case identifier and an immutable version identifier. Compilation resolves each edge to an exact artifact digest, claim revision, evaluation envelope, policy version, safeguard record, or authority record. The compiled view records whether each dependency is current for the declared deployment context. “Current” means identity and applicability match the case boundary; it does not mean the evidence is true or sufficient.

A material dependency change creates a successor case version. Changes include a new model or adapter, a different access mode, an expanded user population, a revised hazard model, a superseded evaluation, a changed safeguard, a new defeater, or an altered acceptance criterion. The predecessor remains available with the decision and evidence that existed at the time. A successor cannot silently inherit a favorable status: affected edges return to review, while unaffected subarguments may retain their recorded state with explicit lineage.

The lifecycle has four distinct verbs. Compile checks identities and required fields. Challenge adds a defeater, countercase, dissent, or scope objection. Review records a bounded judgment by an identified reviewer under a declared independence condition. Decide belongs to the existing readiness and authority system. Conflating these verbs creates the most dangerous form of argument theater: a successful compilation is described as an accepted case, and an accepted case is described as permission to release.

75.7.3 Worked trace: a stale control result and an unresolved defeater

Consider a synthetic case whose top claim concerns model M7, tool profile T-readonly, hazard family H-exfiltration, and a 30-day evaluation window. Its control subargument cites a monitor evaluation for model M6 and the same named tool profile. The case also contains a countercase asserting that a new adapter changes what the monitor observes. The release path is requested, but the countercase has no resolution record.

Step	Incoming record	Compiler observation	Required route	What is not inferred
1	Bounded top claim and deployment context	Case identity and affected path are syntactically complete.	Continue compilation.	The hazard model is not shown complete.
2	Monitor result for `M6`	Model identity does not match `M7`; the evidence dependency is stale for this case.	`requireEvidenceRepair` and retain the prior pointer.	The monitor is not judged ineffective, and `M7` is not judged unsafe.
3	Adapter countercase	The challenge applies to the control edge and is unresolved.	`requireAccountableReview`; the affected release cannot reach readiness review.	The countercase is not presumed correct.
4	Proposed replacement evaluation	New evidence receives a new digest and envelope; it cannot overwrite the stale record.	Recompile a successor case and request independent review.	A passing score is not evidence adequacy or release authority.
5	Reviewer resolves the challenge	Resolution, rationale, scope, dissent, and residual owner are recorded.	If every earlier boundary is complete, emit only `releaseToReadinessReview`.	The case does not release the system.

This trace matters because “block” has several meanings. A stale pointer blocks case progression until evidence identity is repaired. An unresolved defeater blocks the affected readiness route until accountable review. Neither is a scientific conclusion about system safety. The route records what the process must do next and preserves enough history to audit whether the response was appropriate.

flowchart LR
  B["Deployment, hazard, and authority boundary"] --> C["Versioned case graph"]
  C --> G["Scoped claims and strategies"]
  C --> E["Evidence and provenance references"]
  C --> A["Context, assumptions, and acceptance criteria"]
  C --> D["Defeaters, countercases, and residuals"]
  G --> R{"Required support and review complete?"}
  E --> R
  A --> R
  D --> R
  R -->|"no or unresolved"| Q["Repair, accountable review, or affected-path block"]
  R -->|"bounded case status"| H["Existing readiness and authority gates"]
  Q --> L["Case version, dissent, and residual ledger"]
  H --> L

What the assurance flow shows: compilation makes dependencies inspectable. It can preserve a narrow case status and prevent an unresolved case from being mistaken for a release decision. The evidence, evaluation, safeguard, readiness, and authority layers retain ownership of their own truth conditions.

75.8 Interfaces

Evidence States and Claim Discipline owns claim support states and transition review. The case references claim records and cannot promote a claim by presenting it in a graph.
Benchmark Ratchets and Anti-Goodhart Evidence owns benchmark integrity; Adversarial Evaluation, Sandbagging, and Training-Time Deception owns whether the observed behavior can support an argument under its elicitation, monitor, reward, and selection conditions.
Capability Thresholds and Deployment Commitments owns threshold response. A case can identify the commitment it bears on but cannot set, relax, or waive the threshold.
Readiness Gates, Residual Escrow, and Quarantine owns admission, quarantine, and residual custody. An unresolved case routes to those controls rather than deciding its own outcome.
Artifact Graphs, Audit Logs, and Replay owns provenance and replay. Case nodes carry stable pointers and scope claims instead of becoming a duplicate evidence store.
Security Kernel and Runtime Adapters own technical safeguards and action authority. The case can require evidence about them but cannot implement or authorize them.

The complete twelve-owner boundary also preserves Data/Supply-Chain, Formal Proof, Human Intent/Constitutional/Moral/Governance, Resource Economics, Incident/Replacement/Rollback/Release, and Living-Book authority. The case owns only compilation of scoped support and challenge relations. It cannot validate an input, promote evidence, verify a control, accept a residual, close an incident, authorize recovery, word a public claim, or deploy anything.

The interfaces prevent two opposite errors. One is treating the case as a decorative summary that cannot change any workflow. The other is treating it as a super-layer that replaces the detailed evidence and authority systems beneath it. A useful case affects routing by making a gap visible; the underlying owner still decides whether and how that gap can be closed.

75.9 Invariants

Every top claim is bound to deployment context, hazard/threat scope, case version, acceptance criterion, decision authority, and affected release path.
A support edge names the property, evidence reference, strategy, and scope it is asserted to support; visual connectivity does not establish adequacy.
An unresolved defeater, missing countercase review, missing acceptance criterion, or missing residual owner cannot become a favorable conclusion or release clearance.
A rendered, complete, or notation-conformant graph cannot change support state, establish safety, or supply authority to deploy.
A change retains the prior version, rationale, reviewer, affected claims, and re-review trigger.

These invariants make the case a form of disciplined memory. They do not give the compiler privileged knowledge of hazards or truth. They ensure that the conditions for a conclusion remain visible long enough for an independent reviewer to challenge them, and they make a missing condition operationally meaningful rather than merely embarrassing.

The full invariant set additionally requires typed nodes and edges, authoritative source pointers, explicit outside-envelope and search-power limits, retained assumptions and dissent, challenge lineage after resolution, dependency-based review independence, noncollapsed hazard families, state and authority separation, immutable receipts, successor invalidation, accountable redaction, complete case denominators, visible maintenance economics, and the rule that finite routing artifacts establish no real argument or safety conclusion.

75.10 Failure modes

Argument theater: a polished graph has unsupported edges, stale evidence, or omitted assumptions.
Defeater laundering: a case records only favorable evidence and hides countercases, failed evaluations, or dissent.
Scope drift: a case is reused outside its deployment context, hazard model, model version, access conditions, or review period.
Evidence aliasing: a receipt, metric, or theorem is cited as if it proved a broader safety or control claim.
Authority laundering: structural completeness or case acceptance is read as release permission.
Maintenance rot: a graph remains connected to superseded policies, evaluations, safeguards, or residuals.

The complete failure register also covers hazard and countercase theater, reviewer-independence theater, assumption and control laundering, confidence collapse, acceptance and override laundering, in-place version laundering, disclosure failure, unknown-hazard neglect, and case-factory Goodhart pressure.

The response to these failures is not a more elaborate diagram. Unsupported edges require evidence review; hidden countercases require active challenge; scope drift requires a new boundary and re-review; evidence aliasing requires a narrower claim; authority laundering requires a separate release gate; and maintenance rot requires dependency versioning. A case is valuable because it makes each repair route identifiable.

75.11 Consequences and tradeoffs

First, compilation creates a measurable maintenance burden. Every dependency needs an owner, identity, applicability rule, and invalidation trigger. That cost is not incidental: it is the price of preventing a favorable narrative from outliving the evidence that once supported it. A case program should report review queue size, dependency churn, stale-edge age, and reviewer time alongside the number of cases compiled.

Second, a graph increases legibility while also increasing attack surface. If public, it may reveal safeguards, threat hypotheses, or weak dependencies. If private, it may hide disagreement from affected stakeholders. The publication policy therefore needs node-level disclosure classes and a public residual summary, not a choice between total disclosure and a content-free badge.

Third, decomposition can improve disagreement. Reviewers can contest a hazard, strategy, evidence edge, or acceptance condition without rejecting the entire case. But decomposition can also fragment responsibility. The case boundary must retain one accountable decision owner and one owner for each residual; otherwise a graph with many named contributors can leave no one responsible for the conclusion.

Fourth, reuse is both a benefit and a hazard. A well-scoped control argument may be shared across cases, reducing duplicated work. Reuse must be conditional on model identity, environment, access mode, evaluation window, and control version. A reused node that does not re-evaluate those predicates is evidence aliasing, not efficiency.

Fifth, blocking routes can create pressure to weaken the case boundary, omit a defeater, or redefine a dependency as nonmaterial. The audit surface must record scope edits, removed nodes, rejected countercases, and overrides. Governance cost and delay should be measured openly, but speed cannot be improved by deleting the events that explain why a route was blocked.

Sixth, assurance cases concentrate attention on articulated risks. Unknown or politically inconvenient hazards may remain outside the graph. Periodic hazard-model challenge, incident-driven revision, and an explicit “outside the modeled envelope” statement are therefore mandatory complements. Structured assurance can discipline known arguments; it cannot enumerate the unknown.

75.12 Strong objections and residual answers

“A safety case is paperwork that sophisticated developers can game.” This objection has teeth. Typed nodes do not prevent strategic omission or weak evidence. A defensible compiler remains a routing mechanism and makes omissions, countercase handling, dependency versions, overrides, and review independence inspectable and to test whether the workflow rejects known-bad synthetic records. The residual remains: a coordinated organization can still produce a misleading case.

“No finite argument can cover an open-ended system.” Correct. The case is bounded by a named system, context, hazard family, and time window. It must say which harms, modalities, and deployment changes are outside scope. A bounded case may support a bounded decision process; it cannot justify “the system is safe” as a timeless proposition.

“Independent review is only a label when the same institution controls the reviewer.” Also correct. The record can require and describe separation of roles, conflict declarations, access to negative evidence, and the ability to block. It cannot prove psychological or institutional independence. That limitation belongs in the case and in any public claim about review.

“A blocking case compiler becomes an unelected release authority.” It should not. The compiler applies predeclared routing rules and emits a review state. Decision authority remains in the authority ledger, while overrides are explicit, attributable records. The formal route rejecting authority laundering exists precisely because a complete graph must not mint permission.

“Quantification would be clearer than qualitative routes.” A probability can be valuable when its model, data, calibration, and update rules are defensible. A synthetic compiler has none of those. Attaching a number would convert missing evidence into false precision. The current design records support states and exact blockers; later quantitative work would need its own validated measurement model and sensitivity analysis.

“This duplicates the evidence ledger.” Duplication would be a design failure. Case nodes contain stable references, asserted support relationships, and case-local scope; they do not copy or promote the underlying evidence. The source ledger remains authoritative, and a digest or support-state change invalidates the affected case edge.

75.13 Minimum Viable Implementation

75.13.1 Exact current minimum

The repository currently has two public schemas and eight digest-bound synthetic case records: one reaches Readiness Review and seven exercise draft, case-repair, evidence-repair, countercase-review, independent-review, accountable-review, or authority-laundering rejection. Five validator mutations test the bridge. Eight Lean declarations reduce the same hand-authored finite decision tree. No real case, hazard analysis, threat model, evidence-adequacy review, countercase search, safeguard verification, independent institution, acceptance, readiness, release, deployment, incident, reproduction, or transfer ran. The core-claim support effect is exactly zero.

The smallest honest artifact is a versioned assurance-case record. It contains one scoped top claim, deployment and hazard context, argument and evidence references, context and assumptions, known defeaters, countercase-review state, acceptance criterion, residual owner, decision authority, and affected release path. A finite Lean route sends a requested release with an unresolved defeater to accountable review rather than readiness release.

This is a compilation and routing foundation, not a risk model or safety analysis. It does not identify hazards, evaluate a model, establish evidence quality, verify controls, perform independent review, calculate risk, or decide an actual release. A public-safe next slice would compile synthetic case records with one accepted bounded support relation, a stale reference, an unresolved defeater, a missing acceptance criterion, a missing residual owner, and an attempted affected release, retaining a visible result for every route.

This repository implements that public-safe slice as eight synthetic cases with a fixture digest, schema-checked results, eight matching Lean theorems, and five rejecting validator mutations.

75.13.2 Argument-exit campaign

To move beyond argument, preregister natural multi-hazard cases whose governed dependencies, outside-envelope declarations, acceptance criteria, and failure routes are frozen before compilation. Seed omissions, stale edges, scope mismatches, contradictions, control gaps, conflicts, and countercases while retaining every failure and edit. Exercise semantic and evidence-adequacy review, real safeguards, reviewer dependency and conflict controls, multiple argument families, overrides, invalidation, redaction, fallback, rollback, and retirement. Measure structural and semantic fault detection, countercase yield, reviewer disagreement, false clear and false block, resolution latency, burden, maintenance and opportunity cost, and residual age together. Ablate compiler, challenge, review, freshness, and routing mechanisms under matched opportunity, then require independent institutional reproduction and heterogeneous transfer across systems, domains, hazards, access modes, safeguards, evidence regimes, organizations, jurisdictions, and time. Positive, negative, null, inconclusive, narrowed, refuted, withdrawn, overridden, retired, and blocked-after-full-attempt outcomes remain terminal evidence.

75.13.3 Prospective measurement contract

The implemented bridge measures only deterministic agreement among a JSON fixture, a Python route function, a result record, and theorem declarations. Its primary outcomes are route agreement, fixture digest agreement, theorem presence, schema validity, preserved non-claims, and rejection of deliberate corruptions. A run passes only when all eight cases take their declared routes, all eight theorem names exist in the owned module, support-state effect remains none, and mutations that delete a case, alter the digest, claim promotion, remove a theorem, or erase non-claims are rejected.

A later real case-compilation campaign must be preregistered before inspecting outcomes. It should freeze the case cohort, independent-review criterion, dependency-currentness rule, expected failure routes, disclosure policy, time budget, and acceptance threshold. It should report case completion rate, stale-edge detection precision and recall on seeded faults, countercase yield, reviewer disagreement, time to resolution, override rate, residual age, and governance cost together. Success on structural metrics would establish only compiler and workflow behavior. Evidence adequacy, hazard completeness, control effectiveness, safety, readiness, and authority require separate evidence.

75.14 Mature Research Target

The mature endpoint is a continuously compiled assurance control plane. It builds a versioned case from the system’s claim, evidence, evaluation, threshold, safeguard, readiness, provenance, and residual records; recognizes stale dependencies, contradiction, changed deployment conditions, missing countercase searches, and evidence-scope mismatch; and asks the appropriate independent reviewer to inspect the affected argument before any existing gate can progress.

At that endpoint, assurance is not a single confidence number. Different harm models retain different arguments, control assumptions, evidence boundaries, and unresolved questions. A case can be challenged by a new red-team result, a weaker evaluation envelope, a failed safeguard check, or an altered release context without discarding unrelated evidence. Dissent and failed arguments remain part of the decision history, allowing later reviewers to see why a conclusion changed.

Public artifacts would show the case boundary, version lineage, claims, strategies, evidence references, assumptions, active defeaters, countercase searches, review decisions, residuals, and affected release paths. The result would be more inspectable than a policy memo while remaining candid about what the graph cannot establish. It is a target architecture, not a claim that this repository has a complete case, valid threat model, adequate evidence, effective controls, safe system, or authorized deployment.

75.15 Codex test plan

Test	Purpose	Status
Complete bounded record	Emit only readiness review, never release authority.	Implemented in Lean and the synthetic bridge.
Boundary and hazard negative controls	Retain an unbounded record as draft or require case repair.	Implemented in Lean and the synthetic bridge.
Stale dependency route	Send a stale evidence dependency to evidence repair.	Implemented in Lean and the synthetic bridge.
Countercase and independent-review routes	Prevent progression when challenge review or independent review is absent.	Implemented in Lean and the synthetic bridge.
Defeater and residual route	Send an unresolved challenge or ownerless residual to accountable review.	Implemented in Lean and the synthetic bridge.
Authority-laundering negative control	Reject a requested path when case status is treated as release authority.	Implemented in Lean and the synthetic bridge.
Versioned lifecycle and invalidation	Bind case identity through scope, evidence, challenge, review, and readiness handoff; require affected-path and descendant invalidation before returning a readiness-bound case to challenge.	Implemented in `AsiStackProofs.SafetyCaseRefinement`; exact 8-case suite, 30 routes, and 35/35 mutations pass locally with no support or external effect.
Real public-safe assurance workflow	Compile and independently review actual bounded case fragments under preregistration.	Not run; exact campaign contract is specified above.

75.16 Formalization hooks

Tag	Status	Scope
`lean:safety_cases.complete_case.reaches_readiness_review`	implemented	A complete finite record reaches only the pre-existing readiness-review boundary.
`lean:safety_cases.missing_context.retains_draft`	implemented	A record without deployment context remains a draft.
`lean:safety_cases.missing_hazard.requires_case_repair`	implemented	A record without a hazard model cannot progress.
`lean:safety_cases.stale_evidence.requires_repair`	implemented	A stale evidence dependency routes to evidence repair.
`lean:safety_cases.missing_countercase.requires_review`	implemented	Missing countercase review has a dedicated review route.
`lean:safety_cases.missing_independent_review.requires_review`	implemented	Missing independent review cannot reach readiness review.
`lean:safety_cases.unresolved_defeater.blocks_affected_release`	implemented	An unresolved defeater routes to accountable review.
`lean:safety_cases.case_status.cannot_authorize_release`	implemented	Missing separation between case status and authority is rejected.

These finite formal routes do not prove that a defeater is correct, that a case is valid, that evidence is adequate, that a threat model is complete, that a reviewer is independent, that a control works, that a system is safe, or that a release may proceed. They establish only deterministic consequences of the modeled Boolean record and preserve a separate readiness-review boundary.

AsiStackProofs.SafetyCaseRefinement now supplies the stronger consumer model for all eight hooks. It preserves exact case/version, context, claim, hazard, evidence, countercase, reviewer, authority, and residual identity across six reachable stages. A complete record emits only a readiness handoff. A later invalidation needs a cause, affected paths, and complete descendant invalidation, then returns the case to challenge. The independent consumer reruns the original eight fixtures, reaches all 30 routes, rejects all 35 registered mutations, and records zero support assignments and zero external effects.

75.16.1 Formal adequacy audit

The original eight declarations remain useful finite route-precedence and authority-separation regressions, but they are reductions of one hand-authored SafetyCaseRouteFor tree. The refinement adds reachable versioned state, identity custody, rejection-without-mutation, explicit handoff accounting, and challenge re-entry after invalidation; it still does not formalize argument semantics, hazard completeness, causal risk, evidence adequacy, reviewer independence, control behavior, uncertainty, institutional incentives, runtime enforcement, or deployment effects. Its authority ends at one finite authored lifecycle and local consumer.

75.17 Source crosswalk

Source	Chapter use	Boundary
`ext_gsn_community_standard_2011`	Comparator for explicit claims, strategies, evidence references, context, assumptions, justifications, and support relations.	No local GSN case, evidence adequacy, safety proof, readiness conclusion, or release authority.
`ext_evaluations_safety_cases_scheming_2024`	Comparator for scoped unacceptable-outcome claims, incapability/harm/control/alignment arguments, evaluation assumptions, and open gaps.	No local scheming result, alignment result, control evaluation, safety claim, readiness decision, or deployment result.
`ext_aisi_safety_cases_2024`	Comparator for countercase search, negative evidence, uncertainty, disagreement, and confidence limits.	No local countercase adequacy, review independence, safety-case confidence, control efficacy, safety, readiness, or authority result.
`benchmaxxing`	Local conceptual comparator for benchmark lifecycle, regression, residual, and anti-Goodhart records that an assurance graph may reference.	No local case, hazard analysis, evidence adequacy, safety, readiness, release authority, or deployment result.

75.18 Summary

Safety cases make an argument inspectable. They connect a bounded claim to the reasoning, evidence, assumptions, threat model, countercases, and residuals that the claim depends on. That connection is valuable because a complex system’s artifacts rarely speak for themselves, especially when their limits and disagreements point in different directions.

The case adds discipline without taking ownership away from the systems that produce its inputs. It cannot certify a benchmark, validate a proof’s modeling choice, approve a safeguard, or authorize a release. It can expose where a proposed conclusion relies on one of those acts and stop an affected path when the dependency remains unresolved.

Policy Optimization and Learning from Feedback can then consume only feedback and argument status that remain bounded by their source evidence, unresolved defeaters, and authority conditions. Learning should update behavior from a reviewable case state, not from a convenient narrative about safety.

75.19 Evidence reconciliation (2026-07-16)

The invariant protocol, field meanings, and inference limits are stated once in Living Book Methodology. This packet contains only the chapter-specific projection; its authoritative per-atom rows are the safety-cases-and-structured-assurance slice of experiments/claim_family_terminal_coverage/results/result.json.

The core remains blocked after full attempt at argument support. The strongest family attempt was Full-state update and unlearning causal campaign. Its exact boundary is: Broad unlearning claim is narrowed with no support promotion; behavioral removal is not influence, privacy, legal, storage, backup, or descendant erasure. Across 79 atoms, the terminal ledger records 79 blocked_after_full_attempt.

Chapter-specific field	Value
Family / atom denominator	`CF-07` / 79 atoms
Terminal dispositions	79 `blocked_after_full_attempt`
Core	`safety-cases-and-structured-assurance.core`: `blocked_after_full_attempt` at `argument`
Core attempted / missing lanes	`causal`, `empirical`, `executable`, `formal`, `source-synthesis` / `normative`, `transfer`
Attempted local lanes	`causal`, `empirical`, `executable`, `formal`, `source-synthesis`
Missing or unproved lanes	`normative`, `transfer`
Strongest family bundle	Full-state update and unlearning causal campaign (`end_to_end`): One adequate five-seed, seven-arm terminal campaign preserving two prior instrument failures and separate behavioral, influence, privacy, lineage, storage, backup, and descendant axes.
Negative controls	deletion retrain comparator; approximate mitigation arms; 15 rejecting mutations; failure-lineage preservation.
Accepted transitions	none
Maximum inference	Broad unlearning claim is narrowed with no support promotion; behavioral removal is not influence, privacy, legal, storage, backup, or descendant erasure.
Reproduction / next burden	Replay `scripts/validate_p4_m7_update_unlearning_v3.py` and `scripts/validate_claim_family_terminal_program.py`; fill the named atom-specific lanes under a new prospective protocol.

75.20 Handoff

For deployed assurance, Governed Operations, Incident Command, and Graceful Degradation consumes invalidations, incident evidence, recovery obligations, and residual owners without inheriting authority to declare the case complete.

Safety Cases and Structured Assurance compiles the claims, evidence, assumptions, countercases, residuals, and decision boundaries that constrain a release. Content Authenticity, Watermarking, and Synthetic Media Integrity follows by applying that discipline to the generation-to-distribution lifecycle: provenance, watermark evidence, detector calibration, semantic truth, consent, transformations, disclosure, and remedy remain separate. It inherits assurance limits and residual owners, not a claim that signed content is true, unlabeled content is synthetic, a detector generalizes, or a publication channel will preserve the evidence.