The problem
Workflows are increasingly assembled a piece at a time by agents, services and people, and each admitted addition is permanent. An addition can be well formed and pass every local check yet close the last policy-compliant way of finishing: an approval route shut after its alternatives have gone, or a dependency created with nothing left to discharge it. The paper calls this “locally coherent but globally fatal”. Proving one fixed completion would lock the work into a single future, and re-checking from scratch after every step throws away the proof already done.
What the paper does
For any state of the construction the paper defines its “viability residual”: exactly the sequences of future additions that keep the workflow finishable. An addition should be admitted if and only if it lies in that residual, and after an addition the new residual follows from the old one by a simple rule, so step-by-step checks compose into a guarantee for the whole construction.
The residual may be infinite or impossible to compute, so an implementation carries a “certificate” that represents some of those futures, and a trusted checker confirms each update. That is a “proof-carrying stream”: the graph and its certificate advance together, and only the checker has to be trusted, not whatever produced the certificate.
What it shows
If the certificate starts sound and non-empty and every update is checked, every admitted partial workflow can still be completed. The paper also settles what any exact incremental checker must remember: two states with different residuals can never be merged, so grouping states by residual is the coarsest exact abstraction there is, and a finite one exists exactly when there are finitely many distinct residuals.
A worked example shows why the syntax of an addition is not enough. A release can be completed through route A or route B, and an addition closes route A. If B is still open the addition is admitted; if B has already been closed, the identical addition is rejected. The difference lies in the state, not in the addition. The core results, from stream soundness to residual separation, are formalised in Lean 4.
What it does not claim
Viability here is existential: it promises that some acceptable completion remains, not that the workflow will be finished or will run successfully. Additions are assumed deterministic. The exactness results are semantic rather than algorithmic — they say what must be tracked, not how to compute it efficiently — and a cautious certificate may reject additions that were in fact safe. The Lean proofs do not show that any production engine implements the model.
Where it sits
The most recent Opus paper, and the one Kingston presented at ICMAI 2026 at Nazarbayev University in Astana. It presents itself as a synthesis of classical ideas — residual languages, Nerode equivalence, proof-carrying code — rather than claiming them as new, and it is the formal basis of the Opus blog post on why locally valid steps do not guarantee a viable workflow.