World 7 v0.2 — persistent-agent recovery invariants and TLA+ review path
saeed Farokhi
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:
- Single active authority/sequencer for a persistent entity spine.
- CAS-based prevention of lost updates against the current canonical head.
- No rollback of acknowledged external effects; correction must be compensating history.
- Reconstruction from checkpoint + committed event replay must either reproduce a state consistent with identity/history/authority or fail closed.
- 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
saeed Farokhi
Hello TLA+ community,
A brief technical update since my World 7 v0.2 note: the architecture has now been narrowed and frozen as World 8 / Z0-A, and implementation has begun.
The current core is intentionally less metaphorical and more falsifiable. The invariants I would most value formal-methods scrutiny on are now clearer: provider-independent identity, commit-time CAS/stale-writer rejection, fencing, append-only accountable history, intent-bound idempotency, exact effect authorization, proposal ≠ authority, and clean-host restore before renewed write capability.
The reference implementation now includes a versioned operational Skill, a proposal-only Mason, an independent Evaluator and a canonical gateway. The next falsification target is especially useful for formalization: one shared kernel must support two deliberately different Societies — Company and Trading — without weakening those invariants. Trading introduces capital/state races, duplicate-effect risk, ambiguous external execution and reconciliation.
I attached a 26 August technical/scientific dossier. I am not asking for review of the entire document; if anyone is interested, the most useful contribution would be help reducing the core concurrency/recovery rules to a minimal TLA+ model and identifying counterexamples before the two-Society conformance implementation is declared successful.
World 8 DOI: https://doi.org/10.5281/zenodo.22085394
Best regards,
Saeed Farokhi
Academic email: Saeed....@ut.ac.ir
Personal email: sae...@gmail.com