World 7 v0.2 — persistent-agent recovery invariants and TLA+ review path

13 views
Skip to first unread message

saeed Farokhi

unread,
Aug 22, 2026, 2:18:10 PM (2 days ago) Aug 22
to tla...@googlegroups.com

Hello TLA+ community,

I was previously directed by the TLA+ Foundation/Linux Foundation team to this mailing list for technical review of a minimal formal model around persistent AI-agent recovery invariants.

The broader architecture has now advanced and been publicly released as World 7 v0.2:

Zenodo / DOI: https://doi.org/10.5281/zenodo.22058813
GitHub release: https://github.com/saeedfaai/World-v6-public/releases/tag/v7.0.0-rc.1

World 7 treats the AI model as a replaceable cognitive host rather than the owner of identity or canonical state. The current candidate architecture separates persistent identity, authority, append-only event history, reconstructable state, lineage and recovery from individual model providers.

For the formal-methods layer, I am deliberately narrowing the TLA+ target to a small set of safety properties rather than asking for endorsement of the wider architecture:

  1. Single active authority/sequencer for a persistent entity spine.
  2. CAS-based prevention of lost updates against the current canonical head.
  3. No rollback of acknowledged external effects; correction must be compensating history.
  4. Reconstruction from checkpoint + committed event replay must either reproduce a state consistent with identity/history/authority or fail closed.
  5. Lease expiry/failover must not create two simultaneously authoritative incarnations.

The released implementation currently includes bounded local evidence (4,096/4,096 local model assertions and 18/18 seed reference tests), but I explicitly do not treat those results as proof of the distributed properties above. A minimal TLA+ specification and TLC scenarios are intended as the next rigorous verification step.

If anyone in the community is interested in reviewing the state-machine decomposition or collaborating on the smallest useful specification/counterexample set, I would be grateful for technical feedback.

Best regards,
Saeed Farokhi
Independent Researcher
sae...@gmail.com

Reply all
Reply to author
Forward
0 new messages