该论文针对无状态 UTXO（未花费交易输出）风格的账本执行模型提出了一套名为「递归不变量」（Recursive Invariants, RI）的交易级逻辑与工具链，用以支撑多步工作流。背景问题是：UTXO 模型只依据本地数据和被引用数据即可验证交易，天然支持并行验证，且序列化体积/权重可预测；但多步业务流程必须显式地把状态在输出中逐级传递。作者指出一个关键缺口——预先构造好的「下一步交易」可能因为另一笔合法的花费先被确认而失效，于是链下跟踪、冲突处理与交易重建等一致性维护负担被推到了协议边界，带来协调成本与时延上升。 RI 的核心思路是：把工作流规则写成对某笔交易的输入与被索引的后继位置的谓词（predicate），而不是把可执行逻辑或共享可变状态附着在输出上。当某个被引用的后继交易被接受时，被接受交易会在「一步之后」重新检查其前驱的 RI，从而把工作流规则向前携带；连续的单步检查既保持了验证期局部性，又使验证工作可被明确归责与计量。由于许多后继子句在当前交易被验证时并不可判定，作者设计了一个小型静态类型 DSL，采用 Kleene 式三值语义（真、假、未知），把依赖未来的义务推迟到可检查的时刻。 论文形式化了该模型下的 UTXO 验证与账本扩展规则，刻画了「验证期可求值的一步片段」，证明了演绎系统相对三值语义的可靠性（soundness），并给出对应的交易验证算法与账本扩展算法。一个原型 RI 解释器与基准测试工具链评估了六个源自实践的流程；报告出的轨迹显示累计验证成本代理指标近似线性增长，同时展示了分阶段约束能力，且无需为每一步预先承诺一个已构造好的后继交易。 适合读者：区块链协议与智能合约研究者、UTXO/无状态执行模型的设计者、形式化方法与程序语言（三值语义、类型系统）方向的研究者，以及关注交易验证可并行性、可计量性与链下协调成本的工程团队。