Engineering translation of the formal theorems
The paper §4.4 gives 6 core metatheoretical theorems. We do not list the proofs here; we only translate each theorem into "what it means for a real Agent Runtime". Understanding Confluence is the key to understanding the value of the entire paper.
Engineering translation table of the six theorems
[Paper's original conclusion §4.4]
| Theorem | Section | Engineering translation |
|---|---|---|
| Preservation (Thm 59) | §4.4.1 | After any rule application, the registry remains well-formed: parent pointers stay within the registry, provisions of different fibers are disjoint, and the committed view only points to installed fibers. Engineering meaning: the runtime will never be in a state with "dangling fiber references" or "two plugins both claiming to provide 'database'". |
| Recovery Exactness (Thm 61) | §4.4.2 | Under the pairwise independence assumption, for a fiber n's episode [b, u], applying its accumulator is equivalent to the state "n was never loaded" (up to control fields). Engineering meaning: after unloading a plugin, the environment state is equivalent to it never having existed — crucial for HMR and plugin hot replacement. |
| Ordering (Thm 63) | §4.4.3 | Providers must activate before Consumers and unload after Consumers; the dependency resolution (committed view) a Consumer reads throughout an episode is invariant. Engineering meaning: connection pools are not closed until all connections are returned; databases are not closed until all transactions have committed; no "race condition where the consumer reads a half-closed provider". |
| Resolution Coherence (Thm 64) | §4.4.3 | All iterations of a transition run under the same committed view; if target changes mid-way, either the transition completes into Active, or it enters Unloading via L-Divert/L-Raise and rolls back completely. Engineering meaning: no "half old, half new" while loading components asynchronously — part of the effects cannot use old dependencies while another part uses new ones. |
| Progress (Thm 66) | §4.4.4 | Under the assumptions that ≺ is acyclic, len(e_n) ≤ K, and fiber names are finite, a non-quiescent state always has a rule that can fire, and the number of steps per fiber is bounded. Engineering meaning: the system cannot deadlock (guards always release); each configuration change eventually reaches a stable state. |
| Confluence (Thm 73) | §4.4.5 | Under the assumptions of pairwise independence, component total on provision, and no failure, no matter how many loads/unloads/replacements occur, as long as the final configuration is the same, the stable state is equivalent to a single fresh start from that final configuration. Engineering meaning: dynamic history leaves no trace — after an Agent has repeatedly replaced its own components, it is equivalent to a one-shot startup of the final configuration. This is the theoretical cornerstone of the "self-evolving Agent". |
Confluence: dynamic history leaves no trace
Confluence is the climax of this theory and deserves a separate exposition.
Intuitive statement: after the system undergoes any number of dynamic loads, unloads, and replacements, as long as the final configuration is the same, its stable state should be equivalent to that obtained by starting fresh from the final configuration.
For a self-evolving Agent, this means: suppose the Agent replaces tool A three times in succession, unloads and reinstalls Skill B twice, and adjusts the isolation realm of sub-Agent C; as long as its final component configuration is the same as that of "some clean start", then the runtime's stable state (which components are active, each one's committed view, the accumulated environment state) is equivalent to that clean start. Dynamic history leaves no trace.
This is a guarantee that other DI/HMR frameworks do not provide:
- Traditional DI does not support runtime replacement, so there is no Confluence to speak of;
- HMR requires developers to hand-write state migration functions, and whether migration is correct has no formal guarantee;
- Container orchestration's "restart = clean" is a coarse-grained discard of all state, not a same-granularity equivalence.
[Paper's original conclusion §4.4.5] Note the preconditions of Confluence:
- pairwise independence: effects are independent of each other or commute (Def 19);
- component total on provision: every component actually installs all the keys it declares (Def 69);
- no failure: failure scenarios are excluded.
[Paper's original conclusion §4.4.5] Confluence excludes failure scenarios (L-Raise in §4.3.4) — because failures are a real source of divergence: one schedule may fail while another may succeed, but Cor 62 guarantees that a failed fiber's contribution to state is 0 (a failed component's side effects are fully rolled back and do not affect other fibers). So "failure" does not break state consistency, but it does cause two dynamic paths to diverge (one with a failure, one without).
What this proof does not guarantee
[Paper's original conclusion §6.1, §6.3] The formal proofs only cover side effects managed through the Context. They do not guarantee that:
- The inverses written by developers are necessarily correct (the witness condition
g(δ)=γis an obligation, not verified); - Side effects outside the Context (directly modifying global variables, files, databases, external systems) can be reverted;
- External emissions (network requests, messages, emails, payments) can be automatically rolled back — once emitted, they cross the system boundary;
- The security of untrusted plugins — Context-level access control cannot replace a process/container/WASM sandbox;
- Confluence under failure scenarios (explicitly excluded);
- Version compatibility and structural compatibility of dependency keys (§6.6 open problem).
For detailed preconditions and limitations see Limits and overall evaluation. For how this theory lands on DeepSeek Harness see The relationship with DeepSeek Harness.