Code Contracts: Halfway Between Unit Testing And Formal Verification

AI agents now refactor our code faster than we can review it. They keep the test suite green, but that doesn’t mean the business rules still hold. To ensure that the rules are respected, we need a way to formally specify and verify them. But formal verification is often too heavy for everyday development.

Between unit tests and formal proofs, there is room for a middle ground. In this article, I take a small expense-splitting function, let an agent break it in three different ways, and compare three approaches to catch the bugs:

1. design by contract with Eiffel,
2. prose contracts reviewed by an agent with Code Contracts, and
3. mathematical proofs with Bend.

Introduction To Formal Verification

At the far end of the spectrum sit formal languages. Instead of checking a few cases, you write a specification and a proof for the code you wrote. In a formal language, each sentence has only one possible reading, so there is no ambiguity.

Lean is the de facto standard among proof assistants: mathematicians use it to formalize entire fields of mathematics in Mathlib.

Here is an example Lean function that increments a natural number:

def addOne (n : Nat) : Nat := n + 1

theorem addOne_gt (n : Nat) : addOne n > n := by
  unfold addOne
  omega

The first part is the implementation; the theorem part is the proof that the implementation satisfies the specified property. When the code is compiled, the implementation is verified for every possible value of n, so it’s more powerful than a unit test.

The problem is that writing proofs is a skill of its own. And formal proofs are often longer than the code they verify. So for everyday web development, Lean is often impractical.

A Refactoring Agent That Costs a Lot

To compare verification methods that are stronger than unit tests but more practical than Lean, I need a test case. Having worked in banking, I know that a price gap or a misplaced decimal point can quickly become a big problem.

So I go for a Tricount-style app. It’s an app that lets you add expenses and share them among a number of participants.

Photo: Romain Gal on Unsplash.

The heart of the app is a very simple split function. It works in integer cents (i.e. 1 € is represented as 100). If there is a remainder when dividing the amount by the number of participants, it gives the leftover cents, one by one, to the first participants.

export function split(amount: Cents, participants: string[]): Map<string, Cents> {
  const rest = amount % participants.length;
  const base = (amount - rest) / participants.length;
  return new Map(participants.map((id, i) => [id, base + (i < rest ? 1 : 0)]));
}

Being conscientious, I write a very simple unit test.

test("split 30 € between 3", () => {
  assert.deepEqual(
    [...split(3000, ["anthony", "benoit", "thibault"]).values()],
    [1000, 1000, 1000]
  );
});

Some of you may already see the problem with this test. But remember that this is for the sake of my exploration.

When working with Claude, I regularly use the /simplify command to ask it to review my code and to simplify it if it finds room to do so. In the case of the split function, since I haven’t added any specification to my project, it does simplify the implementation a bit too much, losing the handling of the leftover cents in the process:

export function split(amount: Cents, participants: string[]): Map<string, Cents> {
  const share = Math.round(amount / participants.length);
  return new Map(participants.map((id) => [id, share]));
}

Let’s call this change A. It saves one line of code and the function is a little easier to read. When I rerun the unit test, it still passes:

$ node --test typescript/split.test.ts typescript/add-expense.test.ts
✔ split 30 € between 3
ℹ pass 1
ℹ fail 0

But that’s the problem: my tests are incomplete. I haven’t tested the case where the amount does not divide evenly among participants, so the regression doesn’t show up.

Photo: Roman Wimmers on Unsplash.

If we’re talking about sharing costs within a group of friends, the few cents of difference will, at worst, cost a coffee. But in a banking system, it can hurt quickly.

Regulators watch this. EU Regulation 1103/97 requires rounding to the nearest cent. In France, a lender that states a wrong APR can lose its right to interest (article L341-1 of the Consumer Code).

Unit Tests to the Rescue?

We just saw that our unit test wasn’t perfect. One solution would be to write tests that also cover the cases where cents are left over after the split.

test("split 10 € between 3", () => {
  assert.deepEqual(
    [...split(1000, ["anthony", "benoit", "thibault"]).values()],
    [334, 333, 333]
  );
});

Tadaaa, we’ve solved the missing cents problem! But what happens if we make the split more complex with business rules? Something like this: whoever pays advances the money; if they are one of the participants, they keep the leftover cents. Otherwise, the cents go one by one to the first participants.

The correct implementation for this business rule is as follows:

export function split(amount: Cents, participants: string[], payerId: string): Map<string, Cents> {
  const rest = amount % participants.length;
  const base = (amount - rest) / participants.length;
  const shares = new Map(participants.map((id) => [id, base]));
  if (participants.includes(payerId)) {
    shares.set(payerId, base + rest);
  } else {
    for (const id of participants.slice(0, rest)) shares.set(id, base + 1);
  }
  return shares;
}

I can cover both branches of the if, with one test each:

const friends = ["anthony", "benoit", "thibault"];

test("the payer absorbs the leftover cent", () => {
  assert.deepEqual(
    [...split(1000, friends, "anthony").values()],
    [334, 333, 333]
  );
});

test("without the payer, the first participant gets the cent", () => {
  assert.deepEqual(
    [...split(1000, friends, "zoe").values()],
    [334, 333, 333]
  );
});

Notice that two different use cases return the same result. I know, this seems like a code smell, but bear with me.

I ask Claude to simplify the code again. It assumes that the app always lists the payer first, and adapts the condition accordingly. This is change B:

if (participants.includes(payerId)) {
// The app lists the payer first, so checking the first participant is enough.
if (participants[0] === payerId) {

My two tests still pass:

• In the first, Anthony pays and is listed first: both conditions give the same answer.
• In the second, Zoé doesn’t take part, and both conditions give false.

But my logic is no longer correct when the payer isn’t listed first. Imagine that Benoît pays for the restaurant. split(1000, friends, "benoit") gives 334 cents to Anthony and 333 to Benoît. The total is right, but the cent goes to the wrong person.

I report this to Claude, which fixes the bug, then suggests another simplification that we’ll call change C. It merges the two branches: a single participant absorbs the leftover cents, whether they pay or not.

} else {
  for (const id of participants.slice(0, rest)) shares.set(id, base + 1);
  // Same as the payer branch: one participant absorbs the leftover cents, no loop needed.
  shares.set(participants[0], base + rest);
}

That’s incorrect, but the unit tests still pass: 10 € between 3 leaves a single cent, and the first participant gets it either way. With 10.01 € and without the payer, two cents are left, and Anthony gets both instead of one.

So here is the problem: since I haven’t added a test for every possible position of the payer in the list, I risk missing a bug.

A unit test checks an output for a given input. It doesn’t necessarily guarantee that the function’s logic is correct.

Here are the three changes the agent has made. I’ll refer to them by letter from now on:

Design by Contract to the Rescue

One solution is to use Design by Contract, which allows us to specify the expected behavior of our functions through assertions. The program itself checks these conditions at runtime (which differs from compile-time verification with Lean), on the actual input, helping to catch errors early.

This isn’t a new idea. In 1986, Bertrand Meyer invented the Eiffel language. His goal was to increase the reliability, reusability and quality of software production. Eiffel was designed with Design by Contract in mind. It lets developers write strict rules (preconditions, postconditions and invariants) directly in the code.

Bertrand Meyer in 2012. Photo: orcmid, CC BY 2.0.

• The precondition (require) says what the caller of a function must provide.
• The postcondition (ensure) says what the function guarantees and returns.
• The invariant says what stays true about an object before and after each operation.

If one of these conditions fails, it’s a violation of the contract, so the program stops with an error.

I port split to Eiffel, and I write the business rule as postconditions:

split (amount: INTEGER; participants: ARRAY [INTEGER]; payer: INTEGER): ARRAY [INTEGER]
        -- Share of each member, indexed by member,
        -- zero for non participants.
        -- Each participant gets the same base share.
        -- When `payer` takes part, the payer absorbs
        -- the cents left over; otherwise they go
        -- one each to the first participants.
    require
        positive_amount: amount > 0
        not_empty: not participants.is_empty
        distinct: across participants as p all participants.occurrences (p.item) = 1 end
    local
        base, rest: INTEGER
    do
        create Result.make_filled (0, 1, member_count)
        base := amount // participants.count
        rest := amount \\ participants.count
        across participants as p loop
            Result [p.item] := base
        end
        if participants.has (payer) then
                -- The payer absorbs the leftover cents.
            Result [payer] := base + rest
        else
            across participants as p loop
                if rest > 0 then
                    Result [p.item] := Result [p.item] + 1
                    rest := rest - 1
                end
            end
        end
    ensure
        exact: total (Result) = amount
        payer_absorbs_rest: participants.has (payer) implies
            Result [payer] = amount // participants.count + amount \\ participants.count
        others_get_base: participants.has (payer) implies
            across participants as p all p.item /= payer implies Result [p.item] = amount // participants.count end
        base_or_one_cent_more: not participants.has (payer) implies
            across participants as p all
                Result [p.item] >= amount // participants.count and Result [p.item] <= amount // participants.count + 1
            end
        first_participants_first: not participants.has (payer) implies
            across participants.lower |..| (participants.upper - 1) as i all
                Result [participants [i.item]] >= Result [participants [i.item + 1]]
            end
    end

Let me explain how it works.

Preconditions say what the caller must provide. The require of split has three clauses:

• positive_amount: the amount is positive.
• not_empty: there is at least one participant.
• distinct: no participant appears twice.

Eiffel checks them on entry to the function, before the first line of the do. If one fails, the bug is in the caller, and split hasn’t computed anything yet. A call that asks to split 10 € between nobody stops on not_empty:

$ ./build/tricount no-participant
GROUP               split      not_empty:
<0000000000000000>             Precondition violated.        Fail

Postconditions say what the function guarantees. The ensure of split holds the business rule. Eiffel checks it on exit from the function, before handing Result back to the caller. If a clause fails, the bug is in split.

• exact: no cent is created or lost.
• payer_absorbs_rest and others_get_base: if the payer takes part, they get the base share plus all the leftover cents, wherever they are in the list, and the others get the base share.
• base_or_one_cent_more and first_participants_first: without the payer, everyone gets the base share or one cent more, and the shares never go up along the list. With exact, these two clauses enforce “one cent each to the first participants”.

These clauses don’t say how to compute the shares. They say which shares are acceptable.

The invariant says what stays true about the group. For example:

invariant
    balanced: total (balances) = 0

Eiffel checks the invariant after each operation that modifies the group. My examples only call split, which modifies nothing, so the invariant has nothing to check here.

Then I write a small test file to replay the inputs of my unit tests on the Eiffel version, plus the split of 10.01 € without the payer. It calls split for each input and prints the shares. It contains no expected values: the postconditions judge each result. It intentionally catches each violation with a rescue, to move on to the next input (without it, the program would stop at the first violation, with the full call trace). To print the expected shares of a failing call, it reruns split with the checks turned off.

On the original Eiffel code, all five calls respect the contract:

Then I apply each of the 3 changes to the Eiffel program:

Eiffel catches the problem in all three changes:

Change A: exact fails on four splits out of five.

Change B: payer_absorbs_rest fails when Benoît pays.

Change C: base_or_one_cent_more fails on 10.01 €, the only split that leaves two cents without the payer.

But Eiffel solves the unit-test problem by introducing a new one. Every rule must be formalized in a strict language, and forgetting a clause leaves a hole as silent as a missing test. Contracts also only judge the calls that happen: without the 10.01 € split, change C would have passed.

I’m a web developer at heart, and I mostly write TypeScript. I’m not used to working with formal contracts like Eiffel’s. I don’t see myself rewriting all my code in Eiffel just to get contracts. Is there a way to have the benefits of contracts without changing my entire codebase?

Code Contracts: Natural Language, LLM Verification

Photo: Arnold Francisca on Unsplash.

Code Contracts removes Eiffel’s two obstacles. Contracts are written in plain English, next to the code, in the language you already use: no new syntax, no new compiler. An agent then reviews the code against these contracts.

A contract is a comment. Here are the ones for split, in TypeScript:

/**
 * @cc [owner:anthony,label:product] split-positive-amount
 * Callers MUST pass a positive integer `amount`.
 */
/**
 * @cc [owner:anthony,label:product] split-not-empty
 * Callers MUST pass at least one participant.
 */
/**
 * @cc [owner:anthony,label:product] split-distinct
 * Callers MUST NOT list a participant twice.
 */
/**
 * @cc [owner:anthony,label:product] split-exact
 * The sum of the returned shares MUST equal `amount`: no cent is created or lost.
 */
/**
 * @cc [owner:anthony,label:product] split-payer-absorbs-rest
 * If `payerId` is one of the `participants`, wherever the payer is listed, the payer's share MUST
 * equal the base share plus all the leftover cents.
 */
/**
 * @cc [owner:anthony,label:product] split-others-get-base
 * If `payerId` is one of the `participants`, the share of every other participant MUST equal the
 * base share.
 */
/**
 * @cc [owner:anthony,label:product] split-base-or-one-cent-more
 * If `payerId` is not one of the `participants`, each share MUST equal the base share or the base
 * share plus one cent.
 */
/**
 * @cc [owner:anthony,label:product] split-first-participants-first
 * If `payerId` is not one of the `participants`, the shares MUST never increase along the list
 * order: the extra cents go to the first participants.
 */
export function split(amount: Cents, participants: string[], payerId: string): Map<string, Cents> {

• @cc marks the comment as a contract.
• The brackets carry metadata: owner is notified when the rule changes.
• split-exact is a stable identifier that reports refer to.
• The sentence is the rule. Nothing executes it: a human, the cc-check tool and the agent read it.

Each contract mirrors a clause of the Eiffel version, with the same name:

Code Contracts doesn’t distinguish preconditions from postconditions: each contract is a sentence. To keep the parallel with Eiffel, I write the preconditions about the caller with “Callers MUST”, and the postconditions about what split returns.

The Code Contracts project provides a skill with instructions that tell an agent how to write contracts and review code against them. This means you don’t even have to write these contracts by hand: ask Claude to read split and draft its @cc comments, then review and adjust them. Reviewing a sentence in plain English is much easier than writing a formal clause.

I install the skill for Claude Code with npx skills add https://github.com/spolu/code-contracts, and I wrap the review in npm run verify. The script runs claude -p with read-only tools, reads the VERDICT: line and exits with an error on a violation, like a failing test.

The core of the script fits in a few lines:

prompt="Read the code-contracts skill at $skill and follow its On-demand verification procedure, read-only.
Scope: $scope. If the scope is a .patch file, review the change it describes against the current code,
without applying it. Otherwise audit the scope against its current contracts, without a diff.
End with exactly one of these lines, alone: 'VERDICT: VIOLATIONS' or 'VERDICT: NO VIOLATION'."

report=$(printf '%s\n' "$prompt" | claude -p --output-format text \
  --allowedTools "Read,Glob,Grep,Bash(npx -y @spolu/cc-check:*),Bash(rg:*),Bash(git diff:*)" \
  --disallowedTools "Edit,Write,NotebookEdit")

echo "$report"
case $(echo "$report" | grep -E '^VERDICT: ' | tail -1) in
  "VERDICT: NO VIOLATION") exit 0 ;;
  "VERDICT: VIOLATIONS") exit 1 ;;
  *) exit 2 ;;
esac

--allowedTools limits the agent to reading and searching, and --disallowedTools forbids it from modifying any file. The exit code follows the verdict: 0 with no violation, 1 with one, 2 if the report has no verdict.

The agent runs neither the code nor the tests. It reads the change, then the contracts of the function, of the folder and of the callers. This is more akin to Lean, which performs static verification, while Eiffel judges a result during execution.

I replay the same examples, starting with the original split function. The agent’s review passes:

Then I replay each change. The agent finds every broken contract, each with an example:

Change A: three broken contracts.

Change B: two broken contracts, on the same example.

Change C: one broken contract, on an example the agent picks itself.

For change C, nobody gives the agent the 10.01 € input: it picks it on its own, whereas Eiffel needs it in the test program.

I really like this approach. But it still has some downsides:

• The verdict is probabilistic, not certain. It’s still an LLM and it can be wrong.
• It’s slow to run, especially for many or complex inputs. In CI, it can slow pipelines down.
• It costs money, especially if you use paid services to run the reviews.
• It never actually runs the code; it relies only on analyzing the text.

But when it flags a likely error, we can ask it to generate unit tests that cover all the edge cases it identified. That gives us the best of both worlds: the review to detect problems and the tests to check them concretely. In CI, we would then only run the unit tests.

Pairing It With Bend

Eiffel and Code Contracts each have a flaw:

• Eiffel gives a sure verdict, but only on the calls that happen.
• Code Contracts reasons about inputs beyond the calls that run, but an agent judges, and it can be wrong.

Bend (GitHub) tries to bring together the best of both. It’s a young language, with a syntax close to Python. Its compiler checks mathematical proofs on top of types.

Photo: Vitaly Gariev on Unsplash.

Why Bend and not Lean, the default choice? Bend’s learning curve is gentler for developers familiar with mainstream programming languages, while it still provides strong formal verification capabilities. We can focus on the rules to verify without getting stuck on the intricacies of proof writing. And Bend was designed with AI agents in mind, so to me it feels like the natural choice.

The process has three steps:

1. I write the rule as a law, in LAWS.bend.
2. Claude writes the proof of this law, in PROOF.bend.
3. bend PROOF.bend checks the proof. It prints ALL PROOFS CHECK if it holds, and SOME PROOFS FAIL otherwise.

I rewrite split in Bend. Here is the law “no cent is created or lost”:

law split_exact:
  for +amount: Nat
  for +n: Nat
  for +p: Nat
  {S.sum(S.split(amount, 1n+n, p)) == amount : Nat}

Line by line, it reads:

• for +amount: for every amount.
• for +n: for every number of participants. The law talks about 1n+n participants, so there is at least one.
• for +p: for every position p of the payer, in the list or outside it.
• The last line: the sum of the shares equals the amount.

Claude writes the proof, in PROOF.bend:

def Laws.split_exact(amount, n, p):
  %split_go_sum(Nat.is_lt(p, 1n+n), 1n+n, p, Nat.div(amount, 1n+n), Nat.mod(amount, 1n+n), {==}, mod_go_le(amount, n, 0n, 0n))
    : {_ == amount : Nat}
  %fill_sum(1n+n, Nat.div(amount, 1n+n)) : {Nat.add(Nat.mod(amount, 1n+n), _) == amount : Nat}
  %divmod_go(amount, n, 0n, 0n) : {_ == amount : Nat}
  %mul_zero(1n+n) : {Nat.add(amount, _) == amount : Nat}
  add_zero(amount)

A Bend proof is a series of rewrites. Each line calls lemmas defined earlier in the file.

1. split_go_sum: whether or not the payer takes part, the sum of the shares equals the rest plus n base shares.
2. fill_sum: n base shares make n × base.
3. divmod_go: n × (amount / n) + (amount % n) gives back the amount. It’s the lemma about division, which Bend’s library doesn’t have.
4. mul_zero and add_zero: what remains is amount + 0 == amount, and the proof is done.

I write a law the same way for each of the five Eiffel postconditions. Claude writes their proofs in 16 minutes, with 25 lemmas, and bend PROOF.bend prints ALL PROOFS CHECK.

Then I apply change A:

Change A: the proofs no longer hold.

With change A, the proof no longer holds, and Bend rejects the change. It works! (Note: I haven’t ported changes B and C to the Bend version.)

However, Bend has flaws too:

• The language is young and still in development, and the syntax isn’t the most intuitive.
• The complete proof is long: 340 lines for five laws. Claude writes it, but every change to the code forces you to redo it.
• I haven’t run bend PROOF.bend --verdict, a second, stricter check, which requires installing Lean 4.34.

Conclusion

I really enjoyed going through these different ways of checking a program’s correctness, whether with tests, assertions or formal proofs.

I’ll point out, though, that the split function is fairly simple, and that for this kind of function, tests and assertions can be enough. Formal proofs become really interesting for more complex or critical functions.

And if I had to bring them into a project that needs them, I think I’d rather go for Code Contracts generating unit tests for me automatically. That would let me keep the stack I use most often.

If you have experience with these tools on large applications, feel free to share your feedback!