AUTHREX-ABORT
When the Evidence Fails, Authority Lapses.

When an autonomous system loses the evidence its mission depended on, what should happen to the authority a human granted it before launch? The common answer is that something should take over: a remote operator, a fallback autopilot, a terminal action. Each of those adds a new capability at the exact moment the system is least trustworthy. That is backwards.

AUTHREX takes the opposite position. Authority is granted in advance by a human, bounded by an explicit envelope, and conditioned on evidence. When the evidence degrades, authority contracts. When it fails, authority lapses and the irreversible action is latched down for the remainder of the run. Only a contingency that was authorised in advance may then be requested, and every transition is written to a hash chained record that can be replayed. The system does not acquire authority. It can preserve or contract the envelope a human authored. It cannot expand it.

Each action depends on an explicitly identified evidence set. As predicates degrade, the set of available actions shrinks. When an irreversible action becomes unavailable it is latched down and cannot return during that run. One finding from the model changed the design: communications recovery violated irreversible non reacquisition, not through direct evidence dependency but through a shared lease term. The corrected rule is that a predicate is recoverable only if no irreversible action depends on it directly through required evidence or indirectly through any shared term.

The canonical outcomes are EXECUTE, HANDOFF, ABORT and DELAY. Inhibit and Divert are internal contingencies beneath ABORT, not outcomes. The request surface is exactly Inhibit, Divert and Handoff. SafeState is deferred and not implemented. HOLD is an extension belonging to a different simulation in the program and is out of scope here. There is no destructive action anywhere in that vocabulary, and that absence is the design, not an omission.

Requests to the platform carry a command, an authority epoch, the policy digest and the evidence snapshot identity. Responses are correlated back to the issuing request. Loss, delay, duplication, stale epochs and controller health degradation are all modelled. Controller health is monotone downward within a run, because recovery would widen requestability. Every transition appends a hash chained entry carrying its reason, the scenario digest and the previous record hash. A sealed run can be replayed from its recorded inputs and compared on ledger head, ledger digest, findings, final state and run identity. Tampering with any field inside that integrity scope is detected.

Two TLA+ modules are the accepted baseline and are frozen. AuthorityLapse.tla version 3 covers envelope confinement, adverse step non expansion, irreversible non reacquisition, execution conformity and no unbacked irreversible execution, plus lapsed set monotonicity and latch capture, across twenty one configurations with every property checked in isolation. InterfaceRecord.tla version 1 covers fifteen interface and record obligations plus type invariance across thirty five configurations. The million run soak establishes deterministic replay consistency and absence of cross run divergence under sixteen way parallelism on the tested machine. It is a separate execution environment, not independent verification, and it is not representative platform testing.

The mutation campaign reports seven valid mutants, four detected, three surviving, one invalid, and a mechanical score of 0.57. The mechanical score is not the result. A property closes only when disabling that property's own oracle causes its behavioural mutant to survive again, which proves the property specific control is what detects the fault rather than an incidental failure. By that standard B12 is closed and B14 and B2 are open.

No development package can self issue NASA software classification concurrence, NASA Technical Authority approval, NASA IV&V determination, NASA flight or operational acceptance, a DoD ATO or cATO decision, DoD residual risk acceptance, DoD developmental or operational test acceptance, DoD legal review, DoDD 3000.09 approval where that directive applies to an incorporating system, government certification, or third party independent verification. These remain external determinations and are recorded as not performed. DoDD 3000.09 becomes relevant if a governance layer of this kind is incorporated into an autonomous or semi autonomous weapon system within the directive's scope. The architecture here is not itself such a system, and the correct language is policy alignment where applicable, not compliance.