Two traditions in software engineering have both tried to address the problems of correctness, composition, and scale. Software verification uses formal methods to prove properties of programs — it gives strong, machine-checked guarantees and composes naturally through the call graph, but has historically required specialist expertise and substantial effort. Design by contract annotates functions with preconditions and postconditions in readable, practical form — it makes the intended behaviour explicit at every interface, but has relied on testing rather than proof to check those annotations. Each addressed part of the problem.
With AI discharging proof obligations, these become a single approach. An LLM writes the code and the contracts; a theorem prover checks them. The human writes the specification. The economics of this are explored in a companion post; here the focus is on what compositionality of contracts gives you once proof is cheap.
Software has a comprehension problem as much as a correctness problem. As systems grow, the gap between what a function does and what you have to understand in order to believe that widens. You end up reading implementation details that have nothing to do with the property you care about. This is why code review is hard, why audits are expensive, and why bugs survive for years in codebases that everyone thinks they understand.
AI makes this problem much worse. LLMs write code at rates that make traditional review impossible — a single session can produce thousands of lines that no human has read carefully, and the production pressure to ship means they often never will. The scale problem that already existed in large codebases is now arriving faster than ever, and the gap between what is written and what is understood is widening by default.
Contracts solve this when the proofs compose. A top-level contract states what the system does — its preconditions and guarantees — without reference to how. Sub-contracts state what each component in the call graph does. The sub-contracts exist not to be read by the human, but to enable the prover to verify the top-level claim. You only need to understand the top-level contract. The machinery underneath is for the machine.
This is componentisation in real terms. Not just splitting code into modules, but having a machine-checked guarantee at every interface.
The Example: Exactly-Once Order Fulfilment
Here is the top-level contract for fulfil_order — a function that processes an order exactly once, handling inventory, payment capture, and event emission atomically:
def fulfil_order(order_id: int, worker_id: int) -> int:
"""
axiomander:
requires:
order_id > 0
worker_id > 0
db_get_order_status(order_id) == OrderStatus.READY
db_get_payment_state(order_id) == PaymentState.AUTHORIZED
ensures:
result >= 0
result <= 1
implies(result == 1, db_get_order_status(order_id) == OrderStatus.DONE)
implies(result == 1, db_get_payment_state(order_id) == PaymentState.CAPTURED)
"""This is what the system promises. To use this function correctly, or to reason about whether a caller is safe to deploy, this is all you need. The order must be READY and the payment AUTHORIZED going in. If the result is 1, the order is DONE and the payment is CAPTURED. If it is 0, recovery is safe.
You do not need to read the implementation. You do not need to understand compare-and-set or idempotent payment capture or inventory reservation. Those are the machine’s problem.
The Decomposition
The implementation decomposes into three sub-functions, each with its own contract:
do_reserve_inventory — reserves stock for the order. On failure, no inventory is consumed. This is the no_lost_inventory guarantee: if this step fails, the caller can retry safely.
def do_reserve_inventory(order_id: int) -> int:
"""
axiomander:
requires:
order_id > 0
ensures:
result >= 0
result <= 1
"""do_capture_payment — captures the authorized payment. Idempotent: calling it twice produces the same result as calling it once. No double charges.
def do_capture_payment(order_id: int) -> int:
"""
axiomander:
requires:
order_id > 0
db_get_payment_state(order_id) >= PaymentState.AUTHORIZED
ensures:
result == PaymentState.CAPTURED
db_get_payment_state(order_id) == PaymentState.CAPTURED
"""do_commit_order — the exactly-once linearization point. Uses a compare-and-set to atomically move the order status from READY to DONE. At most one worker can observe result == 1 for a given order, which is what bounds successful fulfilments to exactly one.
def do_commit_order(order_id: int, worker_id: int) -> int:
"""
axiomander:
requires:
order_id > 0
worker_id > 0
ensures:
result >= 0
result <= 1
implies(result == 1, db_get_order_status(order_id) == OrderStatus.DONE)
"""Each of these contracts is verified independently. The top-level contract of fulfil_order is then proved by composing the sub-contracts — the prover discharges the top-level postconditions by reasoning from the guarantees of the three components without looking inside their implementations.
The Theory Layer
Below the sub-functions is a third layer: the database operations — cas_order_status, capture_payment, reserve_inventory, emit_fulfilled_event. Each of these also carries a contract:
def cas_order_status(order_id: int, expect: int, new_status: int) -> int:
"""
axiomander:
requires:
order_id > 0
expect >= OrderStatus.READY
expect <= OrderStatus.DONE
new_status >= OrderStatus.READY
new_status <= OrderStatus.DONE
ensures:
result >= 0
result <= 1
implies(result == 1, db_get_order_status(order_id) == new_status)
implies(result == 0, db_get_order_status(order_id) != new_status)
writes:
order_status
"""These are the axioms of the theory. The verifier treats them as black boxes whose behaviour is exactly their declared contract. This is the same relationship the sub-contracts have to fulfil_order: the implementation does not matter, only the interface.
The frame conditions (reads:, writes:) tell the verifier what state each operation touches. This is how it knows that capture_payment cannot affect order_status, and that cas_order_status cannot affect payment_state. Without frame information, the prover cannot reason across calls.
What This Means for Understanding Software
The contract hierarchy of fulfil_order has three levels, each verified against the layer below:
To understand what fulfil_order does, you read one contract. To trust that the contract is correctly proved, the prover reads the rest. The human and the machine each do the work they are suited for.
This is what compositionality gives you at scale. A large system with a thousand functions and a verified contract hierarchy can be understood at the top level by reading a single document. The sub-contracts are not there to be read — they are there to be checked. The verification guarantees that the top-level claim holds as long as the sub-contracts hold, and the sub-contracts hold as long as the theory layer holds.
Software understood in the large means contracts at every interface, proofs that compose, and humans reading only what they need to. The implementation is the machine’s business.
Some aspects of the formalisation — particularly global invariant preservation and the exactly-once domain effect expressed as a quantified property over execution histories — are still being extended in Axiomander. The architecture is in place. The contracts shown here verify today.