Stateless unspent-transaction-output (UTXO) ledgers validate each transaction from local data, enabling parallel validation and predictable byte-based fees. However, multi-step workflows must thread state across outputs, and a prepared next-step transaction may become stale when another valid spend confirms first. Explicit state threading therefore pushes consistency maintenance, off-chain tracking, and transaction rebuilding onto the protocol boundary, increasing coordination cost, latency, transaction count, and fees. Recursive invariants (RIs), our proposed transaction-level logic and toolchain, address this gap by expressing workflow rules as transaction-level predicates over a transaction’s inputs and a declared set of designated outputs. Modeled this way, an accepted spend of a designated output re-checks the same RI one step later, carrying the workflow rule forward without persistent shared storage or executable output logic. Accordingly, multi-step protocol rules remain transaction-local and cost-accountable, with cross-transaction guarantees obtained by repeated one-step checking. Not-yet-checkable successor clauses are handled by a small statically typed domain-specific language (DSL) with three-valued semantics over {true, false, unknown}, so future-dependent obligations are deferred rather than forced prematurely. Co-designed with this DSL, our framework formalizes UTXO validation and ledger extension, identifies the validation-time-evaluable one-step fragment, and proves soundness of local checking. Here, we also mechanize the formal development in the Coq/Rocq proof assistant. On the systems side, we implement a prototype RI interpreter and DSL toolchain with explicit byte and fee annotations. Workflows across six practice-anchored case studies incur linear-in-step overhead with a small per-step constant, while avoiding much of the ad hoc transaction constraint engineering and off-chain orchestration otherwise required.