Formal Coverage Status · AUTHREX Systems

Faithfulness taxonomy: all twenty modules

A model earns FAITHFUL only by importing and checking the implemented artifact. A taxonomy in which everything is labelled faithful measures nothing; two of twenty is a measurement.

Two FAITHFUL, one faithful on the discrete side with a bounded continuous side, one NOT FAITHFUL, eleven SURROGATE COUNTERMODEL, three SURROGATE WITHDRAWN, two not models of source. SURROGATE results are findings about mechanism classes, not about implemented code, and are labelled accordingly. SATA carries a separate archived TLC result of 523 distinct states at depth 9.

The method: two properties per claim

Each safety claim was written twice: a naive form phrased over the system's own bookkeeping, and a strong form phrased over ground truth the system cannot access. Across independent domains, nine naive forms held and nine strong forms failed. The gap between the two is the finding: the bookkeeping can be satisfied while the ground truth is violated.

The MAIVA quorum defect: faithful, production-located

The one defect located in production source, by the faithful model MAIVA_QUORUM:

const fEff      = Math.floor((nA - 1) / 3);
const quorumReq = 2 * fEff + 1;
const quorumMet = nA >= quorumReq;

The fault bound is derived from the roster size, then the roster size is compared against a threshold built from that bound. A test whose threshold is a function of its own input can only report on itself. Verified: the check is satisfied for every roster size from 1 to 5,000; at n = 1 a single agent constitutes a quorum. Q_NEVER_FAILS held across 12,507,501 distinct states. The Byzantine formula n >= 3f+1 is correct in isolation; the defect is that f must be an independent assumption about the adversary. The scope is bounded to the quorum decision at the named lines; nothing downstream is covered. This is a documented open defect.

Strong-form counterexamples

Writing the MAIVA repair as an executable requirement surfaced R1_ASSUMPTION: the Byzantine repair is sufficient only while actual compromise is bounded by MaxCompromised, and no runtime check can establish that bound. A system cannot verify its own compromise level. Writing a requirement down discovered that the requirement needs an assumption stated beside it.

Status change: Obligation 6 is OPEN

The GLUE property is refuted in the bounded extension. Initial-state correspondence (ABS_INIT_CORRESP) was previously reported as holding and has been WITHDRAWN as bound-dependent:

The mechanism is readable in the archived source without executing anything:

LockoutRelease ==
    /\ locked /\ tick >= lockExpiry          \* no MaxTick guard
    /\ tick' = tick + 1

LockoutHold ==
    /\ locked /\ tick < lockExpiry /\ tick < MaxTick   \* guarded
    /\ tick' = tick + 1

Both actions increment the tick counter; only one is bounded by the horizon. The release path escapes it, and tick = 5 becomes reachable with MaxTick = 4: Downgrade at tick 3 sets lockExpiry = 4; LockoutHold advances under its guard at tick 4; LockoutRelease then advances on the lock-expiry guard alone. The shipped bound was 3, and the property fails at bound-plus-one. Step 4 of Obligation 6 is NOT DONE for two independent reasons: it checked TypeInvariant rather than correspondence, and its HOLDS was a bounded artifact.

Three withdrawn refutations

Each withdrawal is recorded beside its original rather than replacing it. Each was found by reading an artifact, not by any automated check.

Requirements identified before implementation

Five governance requirements, written as executable specifications before any code implements them, which is the cheapest point to satisfy them:

1. Quorum thresholds must absorb the maximum tolerated fault count, and the fault bound must be an independent assumption rather than derived from the roster.
2. Ledger integrity requires an independent decision count to reconcile against; a hash chain proves what was recorded was not altered and proves nothing about what was never offered.
3. Deception detection must weight agreement, not only disagreement.
4. A deliberation clock must advance only by elapsed time.
5. A re-arm token must be bound to a nonce.

Verification integrity

Configurations compared        62
Distinct-state count matches   62
Verdict matches                62
Differences                     0

The complete configuration set was re-executed on a second operating system and architecture against the sealed results, every run with an isolated metadirectory. This is second-environment confirmation by the same producer. It is not verification by an independent party, and it must not be described as such. One shipped configuration (MQ_Q_NOT_SINGLETON) has never reliably executed: it assigns a defined operator, which one platform rejects and another mis-evaluates; it is recorded as environment-specific and unresolved rather than accepted or denied.

Honest limitations

Nothing on this page claims validation, certification, or verification by any independent party. Every formal result referenced is bounded and model-relative.