Help wanted: modelling stochastic GST as a Markov chain stopping time in TLA+

[Abib Duut]

I'm working on a research spec called SynodEnergy, which extends classical Paxos (Synod) with an energy-awareness layer motivated by solar-battery-powered compute deployments in sub-Saharan Africa. I'm looking for guidance from people with more TLA+ experience on how to model the stochastic synchrony component cleanly.

What the spec already does (working, TLC-verified):

The current spec models a three-level energy state per node (High, Low, Off ) with Drain and Charge actions. The critical property is crash-amnesia: when a node transitions Low → Off, it loses its in-memory vote state. This breaks classical Paxos safety because a node can recover, vote for a different value, and produce two quorums across the execution history.

The safety violation is captured via a history variable chosenHist — a monotonically growing set of values that have ever achieved a quorum — with invariant:

`SafetyInv == Cardinality(chosenHist) <= 1`

TLC successfully finds the counterexample: n1 votes a, n2 votes a (quorum), n1 crashes (amnesia), n1 recovers, n1 votes b, n3 votes b (second quorum) → SafetyInv violated.

A Flush action (writing vote state to stable storage before Low → Off) is the proposed fix, but not yet specified.

What I need help with?

The deeper theoretical contribution is replacing the classical DLS partial synchrony assumption, GST as an adversarially-chosen unknown constant, with GST as a stopping time of a Markov chain over infrastructure power states.

Concretely, the environment cycles between a good set G (nodes powered, network synchronous within Δ) and a bad set B (power loss, messages delayed arbitrarily). The chain is ergodic, so the system re-enters G infinitely often. Liveness is then a statement about the stationary measure π(G) and the expected sojourn time in G — not about a one-shot permanent transition.

My specific questions:

1. What is the right TLA+ idiom for modelling an environment Markov chain alongside a protocol? Should the chain be a separate process in PlusCal, a non-deterministic EnvStep action, or encoded as a probability distribution over next states (acknowledging TLC can't check probabilistic properties natively)?
2. TLC doesn't support probabilistic model checking. Is the right approach to use TLC for the safety properties (no disagreement under any chain trajectory) and then separately use a stochastic model checker — PRISM or Storm — for the liveness properties (consensus is reached with probability 1)? Has anyone done a hybrid TLA+/PRISM workflow?
3. For the liveness property itself: classical TLA+ liveness uses <>[] (eventually always). Under stochastic GST, the right statement is something like "with probability 1, there exists a G-sojourn of sufficient length for consensus to complete." Is there a TLA+ encoding of almost-sure liveness, or does this necessarily push to a probabilistic tool?
4. Is there prior TLA+ work modelling Markov-modulated environments or probabilistic fairness conditions that I should read before reinventing this?

Any pointers to relevant specs, papers, or tools would be very helpful. Thank you very much in advance for the time and consideration. I am also available for 15 mins chat about this via Zoom or Google Meet.

Sincerely, 

Abib