We've written before about how StateKeep migrates running actors when a workflow definition changes — routing by event history fingerprint instead of current state, so two actors sitting in the same state can receive different migration decisions based on how they got there.
What we haven't covered is the formal side of it: why this isn't a heuristic that happens to work most of the time, but a model with axioms and proofs behind it.
The full formal writeup — the axioms, the routing law derived from them, and the proofs of the properties below — is part of an ongoing research effort and isn't public yet. What follows is the shape of the model: precise enough that you can evaluate whether it holds up, without it being a how-to.
The Core Idea
The question at the center of this is simple to state and hard to answer: when a machine definition changes, how do you migrate in-flight actors to the new version without replaying their entire event history?
