Adversarial review request: soundness of a TLA+ state projection after resource exhaustion

Questions
1

Hello,

I’m seeking an adversarial formal-methods review of a narrow abstraction question arising from a TLA+ model-checking run.

The original model, which I call Step 17, stored four append-only histories directly in the TLC state vector:

  • metaHistory
  • independenceHistory
  • claimHistory
  • acceptedHistory

That model became intractable under breadth-first exploration. TLC reached:

  • 1,341,303,893 generated states
  • 1,203,411,537 distinct states
  • 988,359,497 states still left on the queue

before terminating because the disk filled while TLC was merging a fingerprint file.

I am preserving that result as:

RESOURCE-EXHAUSTED / INCOMPLETE

No PASS claim.
No property-failure claim.
No formal-verification-completion claim.

I then created a separately named projected model, Step 17B, that removes only those append-only history sequences from TLC’s state vector while retaining the current-state variables and derived epistemic state.

The forum uploader does not permit ZIP/TLA/CFG attachments, so I’m including the relevant model and results inline. I can provide the complete Step 17B package and TLC evidence bundle externally if useful.

The question I most want challenged is:

For the listed current-state safety properties, is quotienting the original Step 17 states by their append-only verdict histories sound?

I am explicitly not treating that projection as proven.

The removed histories do not appear in transition guards and do not determine future verdict availability or the current derived epistemic state. They were append-only records of already-derived values.

I would particularly value:

  • two original Step 17 states with the same Step 17B projection but different possible future projected behavior;
  • a listed safety property whose truth actually depends on the removed histories;
  • a vacuous invariant;
  • an accidentally omitted or over-constrained transition;
  • a counterexample to the abstraction;
  • an argument that the projection should instead be expressed as a refinement mapping, simulation relation, trace-equivalence relation, or another formal correspondence;
  • any reason a completed TLC pass of Step 17B should not be treated as evidence for the projected current-state model.

A counterexample, objection, failed invariant, or disagreement with the abstraction would be a valuable result.

Projected Step 17B model



---------------- MODULE ChronoRealmRecursiveValidationProjected ----------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS
    Claim0, Claim1,

    ValidatorA, ValidatorB,
    RootVA, RootVB,
    MetaRoot0, MetaRoot1,

    MetaClaimA0, MetaClaimA1,
    MetaClaimB0, MetaClaimB1,

    MetaEvaluator0, MetaEvaluator1,

    Support, Reject,

    Unknown, Supported, Disputed,
    IndependenceUnknown, Independent, Correlated,

    MaxSteps

Claims == {Claim0, Claim1}
Validators == {ValidatorA, ValidatorB}
ValidatorRoots == {RootVA, RootVB}
MetaRoots == {MetaRoot0, MetaRoot1}

MetaClaims ==
    {MetaClaimA0, MetaClaimA1, MetaClaimB0, MetaClaimB1}

MetaEvaluators == {MetaEvaluator0, MetaEvaluator1}
Verdicts == {Support, Reject}
ClaimStates == {Unknown, Supported, Disputed}
IndependenceStates == {IndependenceUnknown, Independent, Correlated}

MetaClaimValidator(mc) ==
    CASE mc = MetaClaimA0 -> ValidatorA
      [] mc = MetaClaimA1 -> ValidatorA
      [] mc = MetaClaimB0 -> ValidatorB
      [] OTHER            -> ValidatorB

MetaClaimRoot(mc) ==
    CASE mc = MetaClaimA0 -> MetaRoot0
      [] mc = MetaClaimB0 -> MetaRoot0
      [] OTHER            -> MetaRoot1

VARIABLES
    step,
    validatorRoot,
    metaVerdicts,
    metaClaimState,
    supportedMetaRootsByValidator,
    validatorIndependence,
    claimVerdicts,
    claimState,
    acceptedClaims

vars ==
    << step,
       validatorRoot,
       metaVerdicts,
       metaClaimState,
       supportedMetaRootsByValidator,
       validatorIndependence,
       claimVerdicts,
       claimState,
       acceptedClaims >>

MetaKeys == MetaEvaluators \X MetaClaims
ClaimKeys == Validators \X Claims

MetaSupporters(mc, mv) ==
    {e \in MetaEvaluators : mv[<<e,mc>>] = Support}

MetaRejecters(mc, mv) ==
    {e \in MetaEvaluators : mv[<<e,mc>>] = Reject}

DerivedMetaClaimState(mc, mv) ==
    IF MetaRejecters(mc,mv) # {}
       THEN Disputed
       ELSE IF MetaSupporters(mc,mv) # {}
               THEN Supported
               ELSE Unknown

SupportedMetaRootsForValidator(v, mv) ==
    {r \in MetaRoots :
       \E mc \in MetaClaims :
         /\ MetaClaimValidator(mc) = v
         /\ MetaClaimRoot(mc) = r
         /\ DerivedMetaClaimState(mc,mv) = Supported}

DerivedValidatorIndependence(mv) ==
    LET a == SupportedMetaRootsForValidator(ValidatorA,mv) IN
    LET b == SupportedMetaRootsForValidator(ValidatorB,mv) IN
        IF a = {} \/ b = {}
           THEN IndependenceUnknown
           ELSE IF a \cap b # {}
                   THEN Correlated
                   ELSE IF Cardinality(a) = 1 /\ Cardinality(b) = 1
                           THEN Independent
                           ELSE IndependenceUnknown

ClaimSupporters(c, cv) ==
    {v \in Validators : cv[<<v,c>>] = Support}

ClaimRejecters(c, cv) ==
    {v \in Validators : cv[<<v,c>>] = Reject}

DerivedClaimState(c, cv, indep) ==
    IF ClaimRejecters(c,cv) # {}
       THEN Disputed
       ELSE IF ClaimSupporters(c,cv) = Validators
               /\ indep = Independent
               THEN Supported
               ELSE Unknown

DerivedAccepted(cv, indep) ==
    {c \in Claims :
       DerivedClaimState(c,cv,indep) = Supported}

IssuedMetaKeys ==
    {k \in MetaKeys : metaVerdicts[k] # "None"}

IssuedClaimKeys ==
    {k \in ClaimKeys : claimVerdicts[k] # "None"}

TypeOK ==
    /\ step \in 0..MaxSteps
    /\ validatorRoot \in [Validators -> ValidatorRoots]
    /\ metaVerdicts \in [MetaKeys -> (Verdicts \cup {"None"})]
    /\ metaClaimState \in [MetaClaims -> ClaimStates]
    /\ supportedMetaRootsByValidator \in [Validators -> SUBSET MetaRoots]
    /\ validatorIndependence \in IndependenceStates
    /\ claimVerdicts \in [ClaimKeys -> (Verdicts \cup {"None"})]
    /\ claimState \in [Claims -> ClaimStates]
    /\ acceptedClaims \in SUBSET Claims

Init ==
    /\ step = 0

    /\ validatorRoot =
         [v \in Validators |->
             IF v = ValidatorA THEN RootVA ELSE RootVB]

    /\ metaVerdicts = [k \in MetaKeys |-> "None"]
    /\ metaClaimState = [mc \in MetaClaims |-> Unknown]

    /\ supportedMetaRootsByValidator =
         [v \in Validators |-> {}]

    /\ validatorIndependence = IndependenceUnknown

    /\ claimVerdicts = [k \in ClaimKeys |-> "None"]
    /\ claimState = [c \in Claims |-> Unknown]
    /\ acceptedClaims = {}

IssueMetaVerdict(e,mc,d) ==
    /\ step < MaxSteps
    /\ e \in MetaEvaluators
    /\ mc \in MetaClaims
    /\ d \in Verdicts
    /\ metaVerdicts[<<e,mc>>] = "None"

    /\ step' = step + 1

    /\ metaVerdicts' =
         [metaVerdicts EXCEPT ![<<e,mc>>] = d]

    /\ metaClaimState' =
         [x \in MetaClaims |->
             DerivedMetaClaimState(x,metaVerdicts')]

    /\ supportedMetaRootsByValidator' =
         [v \in Validators |->
             SupportedMetaRootsForValidator(v,metaVerdicts')]

    /\ validatorIndependence' =
         DerivedValidatorIndependence(metaVerdicts')

    /\ claimState' =
         [c \in Claims |->
             DerivedClaimState(c,claimVerdicts,validatorIndependence')]

    /\ acceptedClaims' =
         DerivedAccepted(claimVerdicts,validatorIndependence')

    /\ UNCHANGED <<validatorRoot,claimVerdicts>>

IssueClaimVerdict(v,c,d) ==
    /\ step < MaxSteps
    /\ v \in Validators
    /\ c \in Claims
    /\ d \in Verdicts
    /\ claimVerdicts[<<v,c>>] = "None"

    /\ step' = step + 1

    /\ claimVerdicts' =
         [claimVerdicts EXCEPT ![<<v,c>>] = d]

    /\ claimState' =
         [x \in Claims |->
             DerivedClaimState(x,claimVerdicts',validatorIndependence)]

    /\ acceptedClaims' =
         DerivedAccepted(claimVerdicts',validatorIndependence)

    /\ UNCHANGED
       <<validatorRoot,
         metaVerdicts,
         metaClaimState,
         supportedMetaRootsByValidator,
         validatorIndependence>>

Next ==
    \/ \E e \in MetaEvaluators, mc \in MetaClaims, d \in Verdicts :
          IssueMetaVerdict(e,mc,d)
    \/ \E v \in Validators, c \in Claims, d \in Verdicts :
          IssueClaimVerdict(v,c,d)

Spec == Init /\ [][Next]_vars

Safety properties



MetaClaimStateExact ==
    \A mc \in MetaClaims :
        metaClaimState[mc] = DerivedMetaClaimState(mc,metaVerdicts)

MetaRootMapExact ==
    \A v \in Validators :
        supportedMetaRootsByValidator[v]
          = SupportedMetaRootsForValidator(v,metaVerdicts)

ValidatorIndependenceExact ==
    validatorIndependence
      = DerivedValidatorIndependence(metaVerdicts)

UnknownDeepProvenanceDoesNotBecomeIndependent ==
    /\ (supportedMetaRootsByValidator[ValidatorA] = {}
        \/ supportedMetaRootsByValidator[ValidatorB] = {})
    =>
    validatorIndependence = IndependenceUnknown

UnknownDeepProvenanceDoesNotBecomeCorrelated ==
    /\ supportedMetaRootsByValidator[ValidatorA] = {}
    /\ supportedMetaRootsByValidator[ValidatorB] = {}
    =>
    validatorIndependence = IndependenceUnknown

SharedSupportedMetaRootMeansCorrelated ==
    supportedMetaRootsByValidator[ValidatorA]
      \cap supportedMetaRootsByValidator[ValidatorB] # {}
    =>
    validatorIndependence = Correlated

DistinctSingletonMetaRootsMeanIndependent ==
    /\ Cardinality(supportedMetaRootsByValidator[ValidatorA]) = 1
    /\ Cardinality(supportedMetaRootsByValidator[ValidatorB]) = 1
    /\ supportedMetaRootsByValidator[ValidatorA]
         # supportedMetaRootsByValidator[ValidatorB]
    =>
    validatorIndependence = Independent

ClaimStateExact ==
    \A c \in Claims :
        claimState[c]
          = DerivedClaimState(c,claimVerdicts,validatorIndependence)

AcceptedExact ==
    acceptedClaims
      = DerivedAccepted(claimVerdicts,validatorIndependence)

NoClaimAcceptanceWhenValidatorIndependenceUnknown ==
    validatorIndependence = IndependenceUnknown
    =>
    acceptedClaims = {}

NoClaimAcceptanceWhenValidatorsCorrelated ==
    validatorIndependence = Correlated
    =>
    acceptedClaims = {}

AcceptanceRequiresEstablishedValidatorIndependence ==
    \A c \in acceptedClaims :
        validatorIndependence = Independent

TwoValidatorSupportsInsufficientWithoutIndependence ==
    \A c \in Claims :
        /\ ClaimSupporters(c,claimVerdicts) = Validators
        /\ validatorIndependence # Independent
        =>
        c \notin acceptedClaims

IndependentClaimRejectionCreatesDispute ==
    \A c \in Claims :
        ClaimRejecters(c,claimVerdicts) # {}
        =>
        claimState[c] = Disputed

StepMatchesIssuedVerdicts ==
    step =
      Cardinality(IssuedMetaKeys)
      + Cardinality(IssuedClaimKeys)

AcceptanceRequiresTwoValidatorSupports ==
    \A c \in acceptedClaims :
        ClaimSupporters(c,claimVerdicts) = Validators

Deep configuration

The deeper configuration uses:



MaxSteps = 12

There are 12 one-shot verdict slots in the model:

  • 8 meta-verdict keys
  • 4 claim-verdict keys

Each slot may remain None, or be assigned Support or Reject.

TLC results

Original Step 17

The history-bearing model did not complete.

Last recorded progress:



Generated states: 1,341,303,893
Distinct states: 1,203,411,537
States left on queue: 988,359,497

Termination:



java.io.IOException:
There is not enough space on the disk

Classification:



RESOURCE-EXHAUSTED / INCOMPLETE

NO PASS CLAIM
NO PROPERTY-FAILURE CLAIM
NO FORMAL-VERIFICATION-COMPLETION CLAIM

Step 17B — MaxSteps = 8



Model checking completed. No error has been found.

2,242,441 states generated
322,545 distinct states found
0 states left on queue

Depth of complete state graph search: 9

Fingerprint collision miss estimates reported by TLC:
calculated (optimistic): 3.4E-8
based on actual fingerprints: 2.0E-8

Finished in 5 seconds.

Step 17B DEEP — MaxSteps = 12



Model checking completed. No error has been found.

4,251,529 states generated
531,441 distinct states found
0 states left on queue

Depth of complete state graph search: 13

Fingerprint collision miss estimates reported by TLC:
calculated (optimistic): 1.1E-7
based on actual fingerprints: 9.6E-8

Finished in 8 seconds.

One structural observation is that:



531,441 = 3^12

which is consistent with 12 projected one-shot verdict slots, each having one of three statuses:



None
Support
Reject

I am treating that as a structural observation about the projected model, not as independent proof that the projection is sound.

What I am not claiming

A completed TLC run of Step 17B establishes the configured invariants for the reachable states of the bounded projected model, subject to TLC’s reported fingerprint collision probability.

It does not by itself establish:

  1. that Step 17 → Step 17B is a formally proven refinement;
  2. that every history-sensitive property of the original model is preserved;
  3. implementation correctness outside the TLA+ model;
  4. independent validation of the broader ChronoRealm project.

The part I most want challenged is therefore not the TLC result itself, but the abstraction:

Are two original Step 17 states that differ only in append-only verdict history observationally equivalent with respect to all future behavior relevant to these current-state safety properties?

If not, I would very much like the counterexample.

Thank you for any critical review you are willing to provide.

Best regards,

Austin Simpkins