Proving Your Workflow Can't Break: Invariant Theory for Production Systems

A workflow tells people what to do. An invariant tells you what must always be true. The difference is the difference between a process document and a specification — one describes intended behavior, the other defines required behavior.

Our production system maintains nine invariants. Every operation, every transition, every concurrent action must preserve all nine. If any operation would violate any invariant, it’s rejected. Not flagged for review. Not logged as an exception. Rejected.

The Nine Invariants

The invariant set covers state validity, transition legality, resource integrity, data immutability, and auditability.

Invariant 1 states that every work order must be in a defined state. There is no null state, no “between stages,” no undefined condition. This sounds obvious but it eliminates an entire class of bugs where items exist in the system without a valid status.

Invariant 2 requires that every state transition must be in the allowed transition set. If the system attempts to move a work order from Batched to ArtReady, the transition is rejected because that pair isn’t in the relation. No exceptions. No manual overrides for “just this one case.”

Invariant 3 enforces non-negative inventory. The stock of any SKU in any bin can never go below zero. This means every inventory decrement must be validated against current levels before execution, and the validation plus decrement must be atomic to prevent race conditions.

Invariant 4 locks personalization data after a defined stage. Once a work order passes into personalization, the customer-specific payload cannot be modified. This prevents the operational nightmare of changing personalization after physical application has begun.

Invariant 5 makes cancellation absorbing. A cancelled work order stays cancelled. No resurrection.

Invariant 6 enforces stage index monotonicity. With the exception of cancellation (which jumps to the terminal state), stage indices can only increase. No backward movement.

Invariant 7 prohibits stage skipping. Transitions must follow the defined relation. You can’t jump from Pending to Packed, even if all intermediate work is theoretically complete. Each stage represents a verification checkpoint.

Invariant 8 requires that every inventory decrement has a corresponding reservation record. You can’t just subtract stock. You have to record what was reserved, for which work order, at what time. This creates the audit trail that makes inventory discrepancies traceable.

Invariant 9 requires that every stage transition is logged in the work order’s history. The history is append-only. You cannot delete or modify historical entries.

Inductive Preservation

We prove invariant preservation inductively. The base case is straightforward: at system initialization (t=0), all work orders are in Pending state, inventory is loaded from a validated snapshot, and no transitions have occurred. All nine invariants hold trivially.

The inductive step proves that if all invariants hold at time t, and the next operation respects the admissible rules, then all invariants hold at time t+1. This proof proceeds invariant by invariant, showing that each one is preserved by the transition function.

The critical insight is that each invariant is preserved by construction. The transition function is designed so that violations are structurally impossible, not just unlikely. Invariant 2 is preserved because the transition function checks the transition relation before executing. Invariant 3 is preserved because inventory decrements are wrapped in conditional checks. Invariant 9 is preserved because the history append happens within the same transaction as the stage transition.

The Concurrency Challenge

Single-threaded invariant preservation is straightforward. The hard problem is concurrency: when multiple operations execute simultaneously on different work orders that share resources (particularly inventory).

Consider two work orders that both need the same SKU. If both check inventory (seeing sufficient stock) and both decrement (each consuming stock), the final inventory might go negative. Violating Invariant 3. This is the classic write-skew anomaly, and it breaks invariants even though each individual operation is correct in isolation.

The solution is conflict-serializable scheduling. We require that any concurrent execution produces the same result as some serial (one-at-a-time) ordering of the same operations. Under strict two-phase locking: where all write locks are acquired before any are released. The conflict graph is guaranteed acyclic, which implies serializability.

The practical implementation uses database-level serializable isolation for any transaction that touches inventory or performs a stage transition. This is more expensive than the default read-committed isolation level, but the cost is necessary. Under weaker isolation, invariants can be violated by concurrent operations even if each operation individually preserves them.

Deadlock Avoidance

Serializable isolation with locking creates deadlock risk. Transaction A locks Work Order 1 and waits for Work Order 2, while Transaction B locks Work Order 2 and waits for Work Order 1. Classical circular wait.

We avoid deadlock through a simple ordering rule: all lock acquisitions within a transaction are ordered by work order ID. Since all transactions acquire locks in the same global order, circular wait is impossible. This is a well-known technique from database theory, but it’s surprisingly rare in production systems because most production systems don’t think of their workflows as concurrent transaction systems.

The deadlock avoidance guarantee means the system never blocks indefinitely. Combined with the livelock freedom from the acyclic state graph, this gives us a strong progress guarantee: every work order makes progress toward a terminal state in finite time, even under concurrent load.

Idempotency as Safety Net

Despite the formal guarantees, real systems experience crashes, network failures, and retries. The idempotency algebra provides the safety net: every job operator is designed so that applying it twice produces the same result as applying it once.

If a stage transition operation crashes after executing but before confirming, the retry will attempt the same transition again. Because the operation is idempotent, the retry either succeeds (if the first attempt didn’t complete) or no-ops (if it did). Either way, invariants are preserved and the work order reaches the correct state.

This is the belt-and-suspenders approach: formal proofs guarantee correctness under normal operation, and idempotency guarantees correctness under abnormal operation. Together, they make the system trustworthy in a way that testing alone cannot achieve.

In Part 4, we’ll tackle the hardest computational problem in the system: batch optimization, which is provably NP-hard and requires approximation strategies that balance computational tractability with operational efficiency.