I want software that brings its own proof

You are told a refund is available. Someone else is told the same thing. Each request fits the budget, but the system has promised more than it has.

Checking each request against the total looks reasonable if an earlier promise has disappeared from the calculation. I want software to rule out that failure before somebody has to deal with it.

If AI makes code, specifications and checks cheaper to produce, I want to spend some of that gain on stronger evidence. Less repetitive verification work should let us demand higher-quality software, including from the dependencies underneath our own code.

One promise, tested

You cannot promise the same budget twice.

An abstract refund-budget model, checked with Z3. These are illustrative units, not transactions from a payment system. Every bar uses the same 0–120 scale.

Available budget 100

0120

60 40

Already reservedStill free

The vertical line marks the budget of 100.

Request one 60 reserved

Paid: 0 · Reserved: 60 · Free: 40

Correct check: paid + reserved + new request ≤ budget

01

The first 60 fits

There are 100 units available. A request reserves 60 of them. Nobody has been paid yet, but only 40 units remain free.

Available budget 100

0120

60 60

Already reservedSecond reservation

The vertical line marks the budget of 100.

Request two 20 over budget

Both requests passed. The combined promise fails.

Faulty check: paid + new request ≤ budget

02

The next 60 also looks fine

The faulty rule checks what has been paid and ignores what is already reserved. The second request passes on its own. Together, the two promises exceed the budget by 20.

Available budget 100

0120

60 40

Already reservedStill free

The vertical line marks the budget of 100.

Request two 60 rejected

The first 60 stays reserved. The remaining 40 stays available.

Correct check: paid + reserved + new request ≤ budget

03

Count the first promise before making another

The corrected rule includes existing reservations. With only 40 free, the second request for 60 cannot proceed. Smaller requests can still fit.

Reserve

Move free budget into a promise.

Settle

Move reserved budget into paid budget.

Release

Move reserved budget back into free budget.

Paid + reserved never exceeds the budget, provided each move obeys the model's rule and happens as one indivisible step.

A test tries a case. This check asks whether a bad case can exist.

The example comes from a small formal-methods experiment in my research. The model records the budget, the amount already paid and the amount reserved. Its promise is that paid and reserved amounts together never exceed the budget, and none of those amounts is negative.

A conventional test could try the two requests above. The Z3 solver can ask a broader question: is there any valid starting state and allowed move that breaks the promise?

For the corrected model, it finds none. The check ranges over mathematical integers, not a sample of refund amounts. Its scope is the model; connecting it to a deployed service is a further engineering job.

The maths that makes the promise hold

An invariant is a statement that must remain true as the system changes. Here it has two parts: the amounts stay non-negative, and money already paid plus money reserved never exceeds the budget.

A state is s = (B, p, q). All three are non-negative integers; the budget B stays fixed.

B

Total budget

p

Already paid

q

Reserved

Invariant I(s): true in every reachable state

p + q ≤ B

Paid money plus existing promises never exceeds the budget.

Reserve

Add a positive amount a only when it fits the free budget.

a ≤ B − p − q

p′ = p
q′ = q + a

Substitute the new values

p′ + q′= p + q + a≤ B

The entry condition is exactly what makes the final inequality hold.

Settle

Pay a positive amount already reserved: 0 < a ≤ q.

p′ = p + a
q′ = q − a

The addition and subtraction cancel

p′ + q′= p + q≤ B

The total commitment stays the same; the reservation becomes a payment.

Release

Cancel a positive amount already reserved: 0 < a ≤ q.

p′ = p
q′ = q − a

The total commitment decreases

p′ + q′= p + q − a≤ B

The bound on a keeps the remaining reservation non-negative.

A prime (′) means “after the move”. The downloaded model calls B, p and q captured, refunded and reserved. These are the same quantities under shorter names.

Start with nothing paid and nothing reserved: p = 0, q = 0, so p + q = 0 ≤ B. That is the base case. Each permitted move above preserves the inequality and non-negativity. By induction, any finite sequence of those moves preserves the promise.

The solver searches for a valid state and allowed move that breaks the promise. It asks for all three conditions together:

1. I(s): the state before the move is valid.
2. T(s, s′): the move obeys its rule.
3. ¬I(s′): the resulting state breaks the invariant.

Here T is the transition relation and ¬ means “not”. The corrected model returns UNSAT: no assignment satisfies that combination. Together with the base case, this supports the preservation argument over the model’s full integer range.

Break the rule on purpose

Remove existing reservations from the guard and Z3 finds a counterexample. The queries also replay the 100/60/60 illustration and confirm that the corrected model permits a positive reservation. Rejecting every request would be safe from overspending but useless.

Another query deliberately uses contradictory starting assumptions. It also reports no bad case, because no case exists at all. That is a specification mistake, not a reassuring guarantee.

These distinctions are visible in the solver results. The downloadable queries let someone repeat the checks. This edition was checked again on 13 September 2026 using Z3 4.13.3.0; the query files match the research source.

The AI can help write the promise too

I do not assume people must forever write specifications while AI merely fills in code. Finding ambiguities, proposing models, generating proofs and looking for counterexamples are all work worth automating.

What matters is how the result is checked. An AI’s confident explanation does not establish that a proposition follows. In a proof assistant such as Lean, a small kernel checks proof terms. This experiment uses a different tool, Z3, to check logical constraints; it did not produce a separately verified Lean proof.

There is evidence behind that ambition. In July 2025, an advanced Gemini Deep Think system scored 35/42 on the International Mathematical Olympiad, reaching gold-medal standard with natural-language solutions graded by IMO coordinators. That is mathematical reasoning assessed by people.

Formal proving has a different test. The June 2026 Pythagoras-Prover paper reports 89.8% on MiniF2F-Test for its 32B Lean prover at pass@32, rising to 93.0% at pass@2048. Those budgets allow 32 or 2,048 candidate proofs per problem; they are not single-attempt accuracy. Performance fell on perturbed statements, so transfer to unfamiliar work remains a real test.

These results make AI-assisted proof work credible; they do not establish that a particular application is safe. The useful arrangement is an AI searching for a solution and an explicit checker deciding whether the resulting proof meets the stated claim. Martin Kleppmann’s December 2025 argument is the economic opportunity I care about: making that work affordable in ordinary building.

Give the expert something to correct between meetings

A precise proof of the wrong requirement still leaves us with the wrong software. I want subject-matter experts to be able to inspect behaviour without repeatedly explaining the same thing in meetings.

NASA’s FRET, the Formal Requirements Elicitation Tool, is a useful starting point. Its open-source repository describes restricted English requirements with corresponding formal logic and visual diagrams, consistency checks and requirement-based test generation. That gives people different ways to challenge what a requirement actually means.

I would use UML, the Unified Modeling Language alongside it: a state diagram for what may happen next, or a sequence diagram for who sends what and when. These are views an expert can annotate asynchronously. FRET and UML are separate tools here; I am proposing linked views, not claiming an automatic integration.

Expert's meaning

“Count the money already promised before accepting another reservation.”

UML transition sketch

Pending→Reserved

approve [amount ≤ free] / reserve(amount)

On approval, move from Pending to Reserved only if the guard holds; then record the reservation.

Mathematical guard

a ≤ B − p − q

For a valid state and positive amount, the same condition used in the proof above.

Illustrative fragment for one request, assuming an atomic transition. This is not the complete request lifecycle, generated FRET output or a verified UML-to-code translation.

Keep the requirement, diagram, examples and checks under the same identifier and revision. An expert’s correction should update that chain, with a visible diff for review. Meetings can then concentrate on unresolved meaning. AI can maintain the translations, while validation asks whether the behaviour matches the real need and verification checks conformance to the agreed specification.

NASA-grade discipline at everyday software cost

By NASA-grade code, I mean the ambition of bringing rigorous engineering within reach of ordinary projects.

In The Power of Ten, Gerard Holzmann of NASA/JPL proposed mechanically checkable rules for safety-critical C: simple control flow without recursion, provable loop bounds, no dynamic allocation after initialisation, checked inputs and return values, and compiler warnings plus static analysis. Such restrictions make code and resource limits easier to analyse.

NASA Langley’s formal-methods programme covers mathematically rigorous specification, design and verification. NASA’s wider software-assurance approach includes analysis, testing, safety work and independent assessment throughout the software life cycle. Formal proof belongs within that broader discipline.

For this budget example, the connection reaches all the way down to arithmetic. A direct machine-integer calculation of paid + reserved + amount could overflow before it is compared with the budget. Given a valid state and positive amount, the same mathematical guard can be written as:

free = budget - paid - reserved
accept only if amount <= free

The invariant makes both subtractions non-negative. If the inputs fit the chosen integer type, an accepted reservation also fits within the budget. The implementation still needs to validate that starting state and perform the check and update atomically; this pseudocode supplies neither concurrency control nor a proof of a compiled program.

This example is not NASA certification or flight-qualified software. It makes one connection between a mathematical promise and an implementation obligation visible.

A proof needs an address in the real system

This model assumes each reservation happens as one indivisible step. If a real service lets two requests read the same free balance before either records its reservation, the implementation has escaped that assumption.

That is why I want a range of verification and validation (V&V) methods aimed at different failure modes:

• Property-based testing and fuzzing explore generated inputs, malformed data and unusual sequences.
• Static analysis and type checks target implementation defects; model checking explores specified state transitions; theorem proving establishes selected claims under explicit assumptions.
• Integration, fault-injection and security tests challenge retries, outages, permissions and the joins between components. Expert review and realistic user scenarios challenge whether the requirements are right.

More passing tools are useful only if they cover different ways to be wrong. Generating a specification and all its tests from the same mistaken assumption can create agreement without correctness. Keep independent examples, counterexamples and human corrections in the evidence.

I would concentrate this effort on core dependencies too: parsers, calculations, permission checks and the libraries many features share. Pin the version, state the behaviour relied on, test its boundary and rerun affected checks when it changes. A verified component still needs its assumptions to hold where it is used.

Inside BESF, I want each release to carry the requirement version, code and dependency versions, checks, results and unresolved assumptions. AI could do much of the repetitive preparation and repair, then bring back the disagreements that need judgement. That is the route to stronger guarantees without making assurance a second exhausting job.

My work with Mechanistic Health makes the need for rigorous assurance especially concrete. In a highly regulated setting, evidence about the implementation must sit alongside the relevant domain validation and regulatory assessment; mathematical correctness cannot substitute for either. This is the development approach I want to pursue, not a claim that this experiment verifies a Mechanistic Health product.

I want the same discipline in my other products because I want to sleep at night, especially when AI helped write the code. I want to be able to open the evidence, see which promises were checked, and know what still needs attention.