Review request: minimal TLA+ model for persistent-agent recovery invariants

[saeed Farokhi]

Hello TLA+ community,

Taylor Waggoner at the Linux Foundation suggested that this mailing list would be the appropriate place to ask for technical review.

I am developing a deliberately small TLA+ model for the recovery core of a persistent software agent. The AI context is secondary; the core problem is a distributed-systems one involving identity, authority, replay, and externally acknowledged effects across crashes and restoration.

I am trying to specify and check three safety properties:

1. Single active incarnation
   For a given persistent identity and epoch, at most one incarnation may hold authority to produce externally visible effects.

2. No rollback of acknowledged effects
   Once an external effect has been acknowledged, recovery or rollback must not erase that effect from history. Any later correction must be represented explicitly as a compensating action.

3. Valid reconstruction
   Restoring a snapshot and replaying accepted events must either reconstruct a state consistent with the identity, epoch, ledger prefix, and authorization policy, or fail explicitly rather than claim continuity.

The failure behaviors I want the model to cover include:

• a crash between local state mutation and event publication;
• stale snapshots;
• duplicated or reordered events;
• two simultaneous restoration attempts;
• lease expiry and epoch fencing;
• replay after partial recovery; and
• compensation after an externally visible effect has already occurred.

The larger project is called Entity Ark, an experimental continuity layer in which durable identity, governed state, permissions, provenance, lifecycle, and recovery evidence live outside any replaceable model. However, I am intentionally separating that broader architecture from this request: I am not asking for endorsement of Entity Ark, only for rigorous review of the formal recovery model and its invariants.

The executable implementation currently has 321 automated tests across 15 test families, including a fresh-machine restore drill. I do not regard those tests as proof of the distributed properties above; the purpose of the TLA+ model is precisely to expose behaviors and counterexamples that implementation testing may miss.

What I would most value from this community is feedback on three questions:

1. Are these invariants stated at the right level, or am I conflating safety properties that should be modeled separately?
2. Is epoch fencing plus an explicit authority/lease relation an appropriate abstraction for preventing two restored incarnations from simultaneously producing effects?
3. What is the cleanest way to model the boundary between an internal event becoming durable and an external side effect becoming irrevocably acknowledged?

I am preparing the minimal .tla specification and TLC configuration for publication and would be glad to share the model, counterexamples, implementation, raw logs, and test artifacts for review.

If anyone on the list is interested in critiquing or refining the model, even a short pointer on the right abstraction would be extremely useful.

Kind regards,
Saeed Farrokhi
M.Sc., Mechanical Engineering, University of Tehran
LinkedIn: https://www.linkedin.com/in/saeedfarokhi
Website: https://taminyaran.com
Email: sae...@gmail.com