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:
metaHistoryindependenceHistoryclaimHistoryacceptedHistory
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:
- that Step 17 → Step 17B is a formally proven refinement;
- that every history-sensitive property of the original model is preserved;
- implementation correctness outside the TLA+ model;
- 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