Summary
These presentation notes from ICMAI 2026 in Astana ask what evidence should accompany an addition to a workflow that is still being built. Valid tasks and connections can leave no acceptable way to finish. The example is a supplier-payment workflow with standard and exception approval routes: permanently closing the standard route preserves a possible completion only in the context where the exception route’s required authorisation can still be supplied.
Completion viability means that some finite sequence of permitted additions can reach an acceptable finished workflow. The construction state must therefore include evidence, permissions and outstanding obligations as well as the graph. The viability residual collects the addition sequences that preserve a way to finish. Committing an addition retains the sequences consistent with that choice and removes their committed prefix, describing how the remaining possibilities change without selecting a single predetermined completion.
A proof-carrying stream maintains a certificate alongside the construction state. Starting from a sound certificate that represents at least one sequence, a trusted checker admits an addition only when the updated certificate remains nonempty and its represented futures, prefixed by that addition, were covered by the previous certificate. This preserves viability after every accepted step. A conservative certificate can still reject a safe addition because it may represent only some of the possibilities the underlying model allows.
Exact incremental tracking has a stronger information requirement. Two states cannot share a proof state if the same future addition sequence would leave one viable and the other unable to finish. Grouping states by identical future viability answers gives the residual quotient, which retains precisely the distinctions exact tracking needs. A finite exact representation exists when there are finitely many distinct residuals; the result supplies neither an efficient way to discover them nor a general decision procedure.
The notes separate these results from implementation claims. Lean checks several residual, certificate-chain and proof-state results, while the quotient and minimum-state arguments are proved in the paper. Applying the theory needs a faithful model, a certificate format and a checker. It does not establish that the deployed Work Knowledge Graph already implements the mechanism, that checking is faster, that construction eventually finishes, or that the completed workflow executes successfully.