Coverage and faithfulness status for the TLA+ modelling work across the AUTHREX architectures. Every result on this page is bounded and model-relative. Nothing here has been validated against hardware, and no independent verification has been performed.
A model of a described mechanism is not a model of an implemented mechanism. Before a module is accepted, four questions are answered in writing: does the rule exist in source and where, has it been read, what does the model discard, and does any discarded feature bear on the property. Two verdicts are permitted. FAITHFUL means a refutation is a finding about the code. SURROGATE COUNTERMODEL means a refutation is a finding about the mechanism class only.
| Module | Verdict |
|---|---|
| ADARA_XSI_EXACT.tla | FAITHFUL |
| MAIVA_QUORUM.tla | FAITHFUL |
| HMAA_Refine.tla | FAITHFUL discrete side, BOUNDED continuous side |
| ADARA_XSI_NEAR.tla | NOT FAITHFUL, near-minimum observation |
| ADARA.tla | SURROGATE COUNTERMODEL |
| ADARA_IMPL_V2.tla | SURROGATE COUNTERMODEL |
| CARA.tla | SURROGATE COUNTERMODEL |
| ENGAGE.tla | SURROGATE COUNTERMODEL |
| ERAM.tla | SURROGATE COUNTERMODEL |
| FLAME.tla | SURROGATE COUNTERMODEL |
| MAIVA.tla | SURROGATE COUNTERMODEL |
| MAIVA_REPAIRED.tla | SURROGATE COUNTERMODEL |
| REDLINE.tla | SURROGATE COUNTERMODEL |
| RTA.tla | SURROGATE COUNTERMODEL |
| TEAM.tla | SURROGATE COUNTERMODEL |
| ADARA_IMPL.tla | SURROGATE, WITHDRAWN |
| HMAA_Hybrid.tla | SURROGATE, WITHDRAWN |
| OBL6.tla | SURROGATE, WITHDRAWN |
| HMAA_Authority_FSM.tla | Not a model, archived source |
| REQUIREMENTS.tla | Not a model of source, requirement specification |
Two of twenty are faithful. That ratio is the useful output of this exercise. A taxonomy in which everything is labelled faithful measures nothing; two of twenty is a measurement. The remaining eighteen produce findings about mechanism classes rather than about implemented code, and are labelled accordingly.
Each safety claim was written twice. The naive form is phrased over the system’s own bookkeeping and restates the implementation. The strong form is phrased over ground truth the model carries and the system cannot access.
Across the program, nine naive forms held and nine strong forms failed, in independent domains. The gap between the two forms is where every defect in this program was found. A claim that a system satisfies its own records is not the same claim as a system being correct.
Three refutations were withdrawn. Each is recorded beside its original rather than replacing it, so the register holds the correction and the error together.
A surrogate presented as a code finding. The model discarded the per-sensor baselines and the standard-deviation divisor used in the implementation, so its refutation could not be a statement about the code.
Imported neither the archived specification nor a hybrid model, extending only the integers. A mechanism demonstration rather than a simulation relation.
Inverted the tier semantics. Level 0 is the highest authority in the archived specification; the model placed a zero ceiling on it.
The GLUE property is refuted in the bounded extension, and initial-state correspondence, previously reported as holding, has been withdrawn as bound-dependent: it holds at MaxTick 3 and is violated at MaxTick 4. The mechanism is readable in the archived source without executing anything. LockoutRelease increments the tick counter under the guard locked /\ tick >= lockExpiry, while LockoutHold increments the same counter under locked /\ tick < lockExpiry /\ tick < MaxTick. Both advance time; only one is bounded by the horizon, and the release path escapes it.
No rate-limited tracking law holds the safe set. Only algebraic projection does.
The complete configuration set was re-executed on a different operating system and processor architecture, with zero differences in state counts or verdicts across 62 comparisons.
This is not independent verification and is not described as such anywhere in this program. The producer is the same in both environments. A different machine closes the environment question; it does not close the authorization question, which requires a party other than the author.
Five governance requirements were identified by the modelling work before any code implements them. Arriving at a requirement before the code exists is the cheapest point at which it can be satisfied.
Nothing in this program has been validated against hardware. All results are model-relative.
Two of twenty modules are FAITHFUL. The remaining eighteen produce findings about mechanism classes, not about implemented code, and are labelled accordingly.
No independent verification has been performed. Second-environment confirmation is real and is a different and weaker claim.
Three refutations were withdrawn. Each was found by reading an artifact, not by any automated check.
Every result is bounded. Larger bounds strengthen bounded results; they do not make them unbounded. One result previously reported as established was shown to be an artifact of its horizon.
Self-assessed TRL 2 to 4. No certification, accreditation, compliance determination, or authorization to operate is claimed or implied by any part of this work.