A lot of the conversation about verification treats it as a binary choice: you either have a proof or you do not. That framing makes it hard to adopt. For a team used to vibecoding — LLM writes the code, you run the tests, ship — the distance to a verified system looks like a chasm.
It is not. There is a gradient from behaviour-driven design through executable contracts to mechanised proof, and each step along that gradient gives you something useful without requiring the next. You can move one rung at a time.
But first, there is a principle worth stating.
The Holographic Principle for Software
There is an idea from theoretical physics called the holographic principle: you can encode everything that happens in a volume of spacetime on the surface that bounds it. The surface is all you need. This is compelling for two reasons. You can only measure at the surface, so a good theory should relate what you can observe to what lies beyond. And it radically reduces what you have to know.
We need the same thing for software. Every function has a surface — its interface contract, the preconditions and postconditions, the frame conditions that say what it reads and what it writes. The implementation is the volume. You should be able to understand what a function does, what it promises, and what effects it has, by reading only the surface. The volume should be the prover’s problem.
This is especially urgent in the AI era. LLMs are writing vast amounts of code at rates that make human review impossible. If the only way to understand a system is to read the implementation, we are already lost — we are already shipping code that nobody has read. The countermeasure is to make the surface enough. The contracts at every interface must tell you everything you need to know to reason about the system, and the proof that the volume obeys the surface must be the machine’s responsibility.
That is what the gradient delivers.
Where Many Teams Start: BDD
Gherkin feature files have been the industry’s dominant answer to “what should this system do?” for over a decade. A scenario looks like this:
Scenario Outline: Happy path transfer
Given a source account "<source>" with balance <source_balance>
And a target account "<target>" with balance <target_balance>
When funds of <amount> are transferred from "<source>" to "<target>"
Then the total balance across all accounts is unchanged
And the source balance decreased by the transfer amount
And the target balance increased by the transfer amount
And all account balances are non-negative
Examples:
| source | target | source_balance | target_balance | amount |
| A1 | A2 | 100 | 50 | 30 |
| B1 | B2 | 1000 | 0 | 500 |This is the first step. Product and engineering agree on a shared description of what the system should do. The scenarios are human-readable. They serve as acceptance tests. And they are already a form of contract — they express preconditions (given), actions (when), and postconditions (then).
The limitation is scope. A Gherkin scenario tests a finite set of concrete examples. The total balance is unchanged for A1→A2 with balances 100 and 50. It says nothing about other amounts, other account pairs, or edge cases you did not think to list. The behaviour is sampled, not specified.
The Next Rung: Executable Contracts
specsaver makes the step from Gherkin to contract a single command. You take the same When clause that appeared in your feature file and bind it to a contract: preconditions, postconditions, invariants, frame conditions, and exception exits, all expressed as plain Python functions.
transfer_contract = Contract(
TransferService.transfer,
args_type=TransferArgs,
feature="transfer.feature",
when='funds of <amount> are transferred from "<source>" to "<target>"',
requires=[
lambda state, args: args.amount > 0,
lambda state, args: args.source_id in state.observed.accounts,
lambda state, args: args.target_id in state.observed.accounts,
],
ensures=[
lambda old_s, args, result, new_s: (
old_s.derived.total_balance == new_s.derived.total_balance
),
lambda old_s, args, result, new_s: (
all(a.balance >= 0 for a in new_s.observed.accounts.values())
),
],
invariants=[
lambda state: all(a.balance >= 0 for a in state.observed.accounts.values()),
],
)This is a qualitative change from BDD. The ensures clause is not a list of examples — it is a predicate that must hold for any valid call. The invariant must hold before and after every call. The writes set declares what the function modifies and, implicitly, what it does not. Gherkin gives you sampled behaviours; contracts give you rules over the entire state space.
Here is the key property that makes adoption possible: contracts in specsaver are executable. The same lambda that says all(a.balance >= 0 for a in new_s.observed.accounts.values()) can be evaluated at runtime against the actual state of the system after the function returns. There is no separate test language. There is no compile-then-run cycle. The contract is the test. You run it against your scenarios, and it tells you whether the behaviour matches.
This is the “fluid style”: contracts expressed as Python functions that can be checked dynamically. You get the benefit of a specification that is stronger than sampled test cases, without requiring a theorem prover. You can take existing code, add contracts incrementally, and start getting violations reported immediately.
The same contract rendered for human review:
state: accounts: Mapping[str, Account] ← observed limits: TransferLimits | None ← observed audit_log: tuple[TransferCompleted, ...] ← observed notif_log: tuple[FundsReceived, ...] ← observed total_balance: int ← derived initial_total: int ← ghost requires: ∀ state, source_id: str, target_id: str, amount: int. amount > 0 ∧ source_id ≠ target_id ∧ source_id ∈ state.accounts ∧ target_id ∈ state.accounts ensures: ∀ old(state), source_id: str, target_id: str, amount: int. ∃ result, state. state.accounts[source_id].balance = old(state).accounts[source_id].balance − amount ∧ state.accounts[target_id].balance = old(state).accounts[target_id].balance + amount ∧ state.audit_log extended by one entry ∧ state.notif_log extended by one entry modifies: writes: state.accounts[source_id].balance state.accounts[target_id].balance state.audit_log state.notif_log reads: state.accounts[source_id].balance state.accounts[source_id].currency state.accounts[target_id].balance state.accounts[target_id].currency invariant: ∀ state. ∀ a ∈ state.accounts.values(). a.balance ≥ 0 derived: total_balance ≜ sum((a.balance for a in state.accounts.values())) exceptions: ∀ old(state), source_id: str, target_id: str, amount: int. when: old(state).accounts[source_id].currency = old(state).accounts[target_id].currency old(state).accounts[source_id].balance < amount raises: exc: InsufficientFundsError ensures: ∃ state. exc.source_id = source_id ∧ exc.amount = amount
The quantifiers, the read/write frame, the invariant that all balances are non-negative, the exception exits with their triggering conditions — all of this is visible in one place. An AI can write the programmatic form; a human reads the rendered form. The same contract that produces this rendering is the same contract that runs as a test.
specsaver trace examples.bank_transfer --verifyThe Top Rung: Mechanised Proof
An executable contract checks that the postcondition held for the particular input you tested. A theorem prover checks that it holds for all possible inputs. The distinction is between it worked for these three examples and the assertion holds for every valid state.
Axiomander is the system that converts specsaver contracts into Rocq proof obligations. In the style we have been developing, contracts expressed as axiomander: docstring blocks or specsaver Contract objects are translated into theorems that the prover discharges against the implementation.
The wiring between specsaver and axiomander is not yet complete — the contract-to-proof pipeline is being built — but the architectural relationship is clear. A specsaver contract is already a predicate over (old_state, args, result, new_state). That is exactly the shape of a postcondition theorem in Rocq. The contract form that works as a dynamic test is the same form the prover uses as a proof obligation.
This is the important thing: the same artifact — the contract — serves at every level of the gradient. You write it once. You get different guarantees depending on how you check it.
Gherkin → concrete examples (all teams)
Contracts → executable rules (teams adopting verification)
Proofs → machine-checked truth (teams ready for full guarantees)The Adoption Strategy
The reason this matters is adoption. Most teams will not start with verification. They will start with one of two things: vibecoding with no formal specification at all, or BDD with Gherkin scenarios that test a few happy paths.
The path forward is this:
-
Add contracts around existing code. You do not need to rewrite anything. A
Contractobject in specsaver references an existing function. The contract runs as an additional test layer alongside your existing test suite. You get runtime enforcement of preconditions, postconditions, and invariants. -
Graduate from sampled tests to universal predicates. Replace the Gherkin
Examplestable — which can never be exhaustive — withensurespredicates that cover the entire input space. The dynamic runner checks them on every test run. You get stronger guarantees immediately, with no new tooling. -
Add the prover when you are ready. When a function is critical enough to justify proof-level guarantees — or when an LLM is writing its implementation and you cannot trust the tests — you wire the same contract through axiomander for mechanical verification.
Each step adds something useful. You do not need to adopt the whole stack at once. You can have contracts on critical functions and Gherkin scenarios on everything else. You can have proofs on the functions that handle money and runtime contracts on the ones that handle presentation.
What changes when you adopt contracts is that the specification becomes a first-class artifact. It lives next to the code. It is the thing you negotiate with the LLM. It is the thing the prover checks. The gradient is there. You walk it at your own pace.