Specs, invariants, and contracts

Many engineering failures are not caused by “wrong code” but by unclear boundaries: one part of a system assumes something that another part does not guarantee. Specs, invariants, and contracts are three related ways to remove that ambiguity.

This note takes a practical stance. It treats formal methods as a spectrum of discipline: from writing down behavioural constraints in reviewable language, to turning those constraints into checks (tests, monitors, or model checks). The goal is to make behaviour explicit enough that failures become diagnosable rather than mysterious.

Quick takeaways

• A spec constrains behaviourIt states what must hold, not how to implement it.
• Invariants are “always true” factsThey are useful because they can be checked at many points in a workflow.
• Contracts define boundariesAssumptions + guarantees prevent components from silently relying on each other’s accidents.
• Write constraints you can refuteA good spec can fail; vacuous constraints create false confidence.
• Use simple examplesA tiny state machine or a few traces often clarifies more than a paragraph of prose.

Problem framing (why it matters)

Systems grow by composition: services call other services, modules call libraries, and user-facing behaviour emerges from many local decisions. The moment you compose, you need a story about what each part is allowed to assume.

Without a clear boundary contract, teams often debug by reconstructing intent from logs and code. That is slow and unreliable. A small amount of spec work changes the shape of incidents: instead of asking “why did it do that?”, you ask “which assumption was violated?”

Key concepts (definitions + mini examples)

Specification

A specification is a statement of required behaviour. It is usually written at the boundary: what a function, service, or protocol promises. A good spec is (1) testable in principle and (2) intentionally incomplete about implementation.

Example (API-level):

POST /charge
- If the request is accepted, the system eventually records one charge.
- If the same idempotency key is reused, the outcome is the same charge (no duplicates).

Note what is not specified: which database is used, how retries are handled internally, or which queue implementation exists.

Invariant

An invariant is a property that should hold across all reachable states of a system. In practice, invariants act as “shape constraints” on state. They are powerful because you can check them at multiple levels: unit tests, runtime assertions, and model checks.

Example (state-level):

Invariant: for each orderId, there is at most one active shipment.
Invariant: account balance never goes negative.

Contract (assume/guarantee)

A contract makes composition explicit: it states what a component assumes about its environment and what it guarantees if those assumptions hold. The reason this framing matters is that many bugs are caused by unstated environment assumptions.

Example (service contract sketch):

Assumes: requests may be retried and duplicated.
Guarantees: operations are idempotent with respect to idempotencyKey.

That contract immediately points to design work: where to store the key, how long to retain it, and which operations need idempotency.

Practical checks (steps/checklist)

1) Identify the boundary

Specs are easiest to write at boundaries: API endpoints, protocol messages, or module interfaces. Pick one boundary and write down the promised behaviour in a small number of bullet points.

2) Turn behaviour into invariants

Translate “what must happen” into statements about state. If the spec says “no duplicates”, there is usually a state constraint that encodes it. This translation is where ambiguity becomes visible.

3) Decide where to check

For each invariant, choose at least one check location:

• TestsConstruct cases that would violate the invariant (duplicates, reorderings, partial failures).
• Runtime assertionsCheck cheap invariants at boundaries where bad state would otherwise propagate.
• MonitoringMeasure “invariant health” using counters (e.g., dedup hits, rejected duplicates).

4) Make assumptions explicit

Write down the environment assumptions in plain language: retries, timeouts, reordering, partial failures. If an assumption is unrealistic, you can now decide whether to strengthen the system or narrow the contract.

Common pitfalls

• Writing requirements that cannot failIf the property holds “by construction” it may be too weak to be useful.
• Specifying the implementationA spec that says “use database X” is usually a design choice, not a behavioural constraint.
• Ignoring failure semanticsMany specs implicitly assume no retries or duplicates; production systems rarely have that luxury.
• Overcomplicating the notationSymbols help only if they reduce ambiguity; they are not a success criterion.
• Not connecting specs to checksA spec with no validation path becomes stale prose.

Related notes

• Model checking primerHow to explore a model and check invariants systematically.
• Session types and protocolsProtocols as interface contracts for message orderings.
• Failure modes, retries, and idempotencyA concrete case where contracts prevent duplicate effects.
• Performance regressions checklistSpecs and invariants help distinguish “expected slow path” from regressions.