Contracts
Contracts are the center of Axiom: machine-readable statements about the valid state of a program.
Backend code is full of rules like “offset is inside the buffer” and “response fits the reserved capacity”. Axiom turns those rules into proof obligations.
| Construct | Responsible side | Meaning |
|---|---|---|
require expr | caller | Precondition; the call is valid only when proven. |
ensure expr | callee | Postcondition that every return path must prove. |
invariant expr | type / loop | A property that must remain true. |
assert expr | compile time | An explicit proof checkpoint. |
runtime_assert expr | runtime | An intentionally retained runtime check. |
assume expr | trusted boundary | A restricted “trust me” operation; this is sus. |
A writer that cannot overflow
1writer:2 view<u8> out3 usize used45 invariant used <= out.size()67 push(u8 value):8 require used < out.size()9 out[used] = value10 used = used + 111 ensure used <= out.size()12END writerMutable caller-owned storage.
Used byte count.
Object invariant.
Caller must prove at least one byte is free.
The index is safe because of the contract.
Advance the cursor.
The implementation proves the invariant still holds.
Runtime input still works
1set_page_size(u32 requested) -> result<u32, request_error>:2 if requested == 0 or requested > 100:3 RETURN error(invalid_page_size)4 assert requested >= 15 assert requested <= 1006 RETURN ok(requested)Reject invalid external input at runtime.
After the branch, this is a proof checkpoint rather than a second runtime check.
The success value is now known to be in 1..100.
Why this resembles SPARK
SPARK treats contracts as proof obligations instead of decorative annotations. Axiom adopts that mindset and extends it into views, memory regions, task effects, and bundle planning.