Writing Invariants as Formal Constraints

A practical guide to defining system invariants before writing code.

What Are Invariants?

Invariants are properties that must always be true in your system. They are:

• Formal — expressed in mathematical or logical notation
• Testable — can be verified programmatically
• Enforced — violations are bugs, not edge cases
• Timeless — true at all points in time (or specified temporal scope)

Invariants are your specification. Code is just an implementation of that spec.

---

Why Write Invariants First?

Without Invariants	With Invariants
”The charge should probably link to an outcome”	∀ Fact(charge) → charge.source_id ≠ null ∧ ∃ Fact(outcome) WHERE outcome.id = charge.source_id
”Don’t modify Facts”	∀ Fact f → f.created_at = f.updated_at
”Configs should be versioned”	∀ Config c1, c2 WHERE c1.id = c2.id AND c1.version = c2.version → c1 = c2

Invariants remove ambiguity. They’re contracts that both humans and machines can verify.

---

Notation Guide

We use first-order logic notation. Here’s the syntax:

Symbol	Meaning	Example
∀	”for all”	∀ x = “for all x”
∃	”there exists”	∃ y = “there exists a y”
→	”implies”	x → y = “if x then y”
∧	”and”	x ∧ y = “x and y”
∨	”or”	x ∨ y = “x or y”
¬	”not”	¬x = “not x”
=	”equals”	x = y
≠	”not equals”	x ≠ y
∈	”in” (set membership)	x ∈ S = “x is in set S”
⊆	”subset of”	A ⊆ B = “A is subset of B”

Temporal operators:

Symbol	Meaning	Example
□	”always”	□(x > 0) = “x is always positive”
◇	”eventually”	◇(status = "complete") = “eventually status becomes complete”
t₁ < t₂	”time ordering”	created_at < updated_at

---

The Framework: 7 Categories of Invariants

1. Existence Invariants

Pattern: “If X exists, then Y must also exist (at the time X is created)”

∀ x ∈ X → ∃ y ∈ Y WHERE condition(x, y)

Important: For z0, existence invariants are point-in-time constraints. When a Fact is created, its references must exist at creation time. This doesn’t mean the referenced Fact must have existed before the system started—it means at the moment of creation, the dependency must be satisfied.

z0 Examples:

// Every charge must reference an outcome that exists at charge creation time
∀ Fact(charge) →
  charge.source_id ≠ null ∧
  ∃ Fact(outcome) WHERE outcome.id = charge.source_id ∧ outcome.timestamp ≤ charge.timestamp

// Every cost must reference an invocation that exists at cost creation time
∀ Fact(cost) →
  cost.source_id ≠ null ∧
  ∃ Fact(invocation) WHERE invocation.id = cost.source_id ∧ invocation.timestamp ≤ cost.timestamp

// Every payout must reference an outcome that exists at payout creation time
∀ Fact(payout) →
  payout.source_id ≠ null ∧
  ∃ Fact(outcome) WHERE outcome.id = payout.source_id ∧ outcome.timestamp ≤ payout.timestamp

// Every Deal must have a Contact
∀ Entity(deal) → contact_id ≠ null ∧ ∃ Entity(contact) WHERE contact.id = deal.contact_id

// Every Deal must have external source (z0 doesn't create Deals)
∀ Entity(deal) → external_source ≠ null ∧ external_id ≠ null

// Every Config-dependent Fact must record the Config version
∀ Fact f WHERE f.type ∈ {charge, payout, outcome, decision} →
  config_id ≠ null ∧ config_version ≠ null

Critical Note on Temporal Ordering:

The existence invariants above enforce referential integrity (if source_id is set, the referenced Fact must exist), but they do NOT enforce temporal ordering. This is intentional.

Why? Because temporal relationships between Facts are business-logic dependent, not platform invariants. Different products have different outcome semantics:

Possible Orderings:

1. Desired Outcome → Invocation → Actual Outcome → Charge

   • Campaign sets goal: “We want appointments”
   • Make call (invocation)
   • Appointment booked (actual outcome)
   • Charge for qualified lead

2. Invocation → Charge → Outcome

   • Make call (invocation)
   • Charge for call minutes immediately
   • Later: appointment scheduled (outcome)

3. Invocation → Outcome → Charge

   • Make call (invocation)
   • Call qualifies (outcome)
   • Charge for qualified call

4. Outcome → Invocation → Charge

   • Desired outcome exists (campaign goal)
   • Invocation attempts to achieve it
   • Charge based on attempt or result

The platform enforces: “If a Fact references another Fact, that referenced Fact must exist.”

The platform does NOT enforce: “Outcomes must precede charges” or “Charges must precede outcomes.”

Temporal ordering is product-specific business logic, not a primitive constraint.

How to derive:

1. List your core entities/events
2. Ask: “What must exist for this to be valid?”
3. Write the constraint

---

(Rest of the document continues with the same structure as before…)