Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking

1 Introduction

• Heavyweight formal notations impose mathematical and maintenance costs, leading teams to rely on informal prose, testing, and debugging.Formal specification can expose design flaws before code exists and make assumptions explicit as invariants.Source: §1 · p. 1
• LLMs can review lightweight-mathematics specifications, flag ambiguities, propose invariants and proofs, and generate code, making the specification the primary artifact and code regenerable output [3] [2].The proposed shift moves validation to the specification, where the paper says design flaws are cheaper to catch.Source: §1 · pp. 1–2

Research questions.

• This study tests transfer to online banking, where money replaces knowledge as the conserved quantity shared with the prior study [6].The paper presents this as initial evidence that the discipline is not tied to one problem.Source: Research questions · p. 2, §1 · p. 2
• Scheduled and recurring transfers stress-test the method: generated code grows markedly while the invariant and its proof remain unchanged.The paper also adds an AI-proposed runtime coverage model and Z interfaces, including an invariant proved over all reachable configurations.Source: Research questions · p. 2

2 Background and Relationship to Prior Work

• Z uses typed set theory and first-order logic; its schemas constrain state or transitions with predicates and correspond to typed interfaces with invariants and operation contracts.The paper chooses Z to make pre/postconditions and state invariants explicit while leaving implementation choices open if contracts are met.Source: §2 · p. 2

Domain

• A conservation invariant preserves a global quantity across operations; here that quantity is money, and such invariants are easy to state, prove by induction, and assert at runtime.The predecessor used conservation of knowledge items.Source: Domain · p. 3
• The discipline's pipeline runs from natural language through lightweight mathematics, invariant proof, Z interfaces, and generated code, but this study formalized Z after generating code.The study reports its historical order while recommending Z-before-code for future applications.Source: Domain · p. 3
• This paper is a companion to [6], which established the method and motivation on an organizational-knowledge-growth simulation; unlike Dafny, it verifies the specification, not generated code, which remains regenerable.Source: Domain · p. 3

• AI reviews the specification for ambiguities and inconsistencies, and the human decides how to resolve them and what to leave to the AI.Source: §3 · p. 3
• The prescribed loop proves the invariant by induction, asserts it at runtime, and fixes state and operations as Z contracts before code generation.Source: §3 · pp. 3–4
• This study instead developed the natural-math specification, proof, and runtime assertion before adding Z as a separate pass; the paper recommends Z-before-code going forward.The authors report the actual order as an observation about practice.Source: §3 · p. 4

4 Case Study A: One-Time Transfer

• The one-time transfer specification assigns accounts to users and balances to accounts, then debits and credits the chosen accounts when funds suffice or leaves balances unchanged otherwise.The source is an online-banking fund-transfer requirement; the simulation uses three users and six accounts.Source: §4 · p. 4, Human prompt (excerpt) · p. 4

Human prompt (excerpt)

• The AI-generated 106-line Python simulation selects a transfer at each discrete stage and executes it only when funds suffice.The authors rely on proving and asserting an invariant rather than line-by-line code inspection.Source: Human prompt (excerpt) · p. 4
• The AI review surfaced specification ambiguities, including the summand for total money, whether negative balances are allowed, and whether the lemma must cover arbitrary account sets and balances.The adopted meaning of total money is the sum of the values of the balance function.Source: Human prompt (excerpt) · pp. 4–5

The invariant, proved.

• The conservation lemma states that the sum of account balances is unchanged by a one-time transfer.The proof uses cancellation of the debit and credit; it does not depend on the source account having enough funds because a rejected transfer leaves balances unchanged.Source: The invariant, proved · p. 5, Proof. Summing B′ over AC and… · p. 5

Proof. Summing B′ over AC and isolating the two affected accounts,

• The simulation asserts equality of the total balance before and after each transfer as a runtime check of the proved invariant.Figure 1 illustrates the conserved total for a representative transfer.Source: Proof. Summing B′ over AC and… · p. 5

• A planned transfer enters P for a future time, persists until due, then executes as an ordinary one-time transfer and leaves P.Recurring transfers are modeled as sequences of ordinary one-time transfers.Source: §5 · p. 5
• Figure 2 traces a transfer scheduled at t=1 for t=3, persisting in P until execution is due.Source: Figure 2
• The generated program grows to 265 lines, about 2.5× the one-time version, but the conservation invariant and its proof remain unchanged.Scheduling modifies P without changing balances, and execution is an ordinary one-time transfer.Source: §5 · p. 6

6 A Runtime Coverage Model for the Invariant

• An invariant that has not failed may still be untested on paths capable of breaking it.Source: §6 · p. 6
• Coverage requires exercising and checking all semantically relevant execution paths that affect the invariant.Source: §6 · p. 6

Human prompt (excerpt)

• The prompt asked what should be checked to determine whether the conservation invariant was covered at runtime.Source: Human prompt (excerpt) · p. 6

• Coverage requires exercising both success and failure cases for each transfer type and transfers across different users and distinct accounts.Source: §1 · p. 6
• The planned-transfer checks cover insertion without balance change, persistence across time steps, and execution when due; multi-transfer stages check the invariant after each transfer.Source: §1 · p. 6
• 100% coverage was reported after review judged the five obligations sufficient to exercise every conservation-breaking path.The reviewed obligations cover success and failure, ownership diversity, the planned-transfer lifecycle, and stages with several transfers.Source: §1 · p. 7
• The coverage model is an addition beyond the predecessor's runtime-assertion approach, with the AI proposal reviewed before generated code instrumented its obligations.Source: §1 · p. 7

• Z schemas were AI-generated and human-reviewed; the paper treats Z as an internal interface layer while keeping natural language plus mathematics as the human-facing form.The authors say they would generate the schemas before code to fix contracts earlier and give the generator a precise target.Source: §7 · p. 7
• Operations use explicit pre/postconditions, with paired success and no-change failure schemas; due planned transfers execute as ordinary balance updates and are removed from P.Source: §7 · pp. 7–8
• Review caught missing ownership constraints linking each declared user to its account; conservation still held, so the proof did not expose the contract gap.Source: §7 · p. 8
• Conservation holds for every configuration in the inductive set reachable from any legal initial configuration through finitely many operation schemas.The induction proof uses balance-preserving updates for one-time transfers and finite compositions of those updates for planned executions.Source: §7 · p. 8
• Given only the natural-language specification, the AI identified major interfaces and explicit contracts but omitted initialization and mixed Z schemas with prose.It also introduced simulation-specific indexing into an interface, leaving a human to curate the contract.Source: §7 · p. 9

Results and Observations

• The observations are case-study evidence, and the code was not inspected line by line as it evolved.Confidence came from specification-level review, the conservation proof, runtime coverage model, and Z contracts.Source: §8 · p. 9
• The same conservation invariant and proof carried over unchanged to scheduled transfers even as the generated code grew substantially.The invariant applies to the online-banking specification, not any particular operation.Source: §8 · p. 9
• The conservation assertion held at every checked stage of every run, as confirmed by inspecting simulation output.Source: §8 · p. 9
• After specification review, the first generated implementation appeared correct because its logged simulation output showed expected behavior, including the per-stage invariant assertion.Correctness was judged from the output, not by reading the generated code.Source: §8 · p. 9
• The AI supplied lower-level invariants not stated by the author and proposed usable Z interfaces from prose.Source: §8 · p. 9
• Past a few pages, the AI sometimes silently dropped tasks or sections, so abstraction, modularity, and decomposition still matter.Source: §8 · p. 9

Discussion, Limitations, and Threats to Validity

• The proofs and runtime assertions establish specification properties and properties of observed executions, but do not formally establish that generated code refines the specification.That refinement step is delegated to the AI; runtime assertions cover only exercised paths, and coverage is argued informally rather than measured independently.Source: §9 · p. 9
• The observations are anecdotal, with no control condition or independent replication, and the same author specified the system and judged correctness.Source: §9 · p. 9
• The “correct on first generation” claim rests on the author's inspection of simulation output rather than an independent oracle, leaving construct validity weak until a measurement protocol is specified.Source: §9 · p. 10
• The work used ChatGPT in the first quarter of 2026, but the underlying model version is unknown, so reruns with another model or at another date may differ.Source: §9 · p. 10
• Whether the approach extends as cleanly to properties without conservation structure, such as liveness or security, remains open.Source: §9 · p. 10

Conclusion and Future Work

• The study replicates the discipline in online banking, adds a runtime coverage model and a Z formalization proved over all reachable configurations, and stress-tests scheduled transfers.Source: §10 · p. 10
• The recurrence of a conservation-invariant spine across knowledge and money is preliminary evidence that the discipline generalizes across domains.Source: §10 · p. 10
• The specification-level proofs and checks do not close the gap to generated code; refinement checking or verified generation is identified as a next step.Source: §10 · p. 10
• Future evaluation includes controlled studies, additional domains, and properties without conservation structure.Scoped extensions include recurring solvency, a liveness/scheduling property, and multiple heterogeneous transfer types.Source: §10 · p. 10
• Although this study formalized Z interfaces after code generation, the authors recommend fixing Z contracts first and treating code as regenerable output.Source: §10 · p. 10
• The AI-generated internal Z layer is intended to sharpen ambiguity detection and help generation scale, but whether it measurably does so remains open.The user-facing form remains lightweight natural language with mathematics.Source: §10 · p. 10
• The authors propose formalizing the discipline as a reusable skill and systematically testing its transfer across agents and use cases.Source: §10 · p. 10

Reproducibility and Artifacts

• Appendix A reproduces prompts and AI replies for each development step, while code links cover the one-time and scheduled simulations and coverage checker.These artifacts support repeating the process or adapting it to another domain or AI agent.Source: Reproducibility and Artifacts · p. 11

Fund transfer - one time transfer

• The initial ChatGPT-generated one-time-transfer simulation was 106 LOC; its execution looked correct, but assertions were added to increase confidence in the implementation.The simulation randomly selected transfer inputs and reported the inputs and operation result.Source: Fund transfer - one time transfer · p. 12

Assertion - the overall money in the system is constant

• The one-time-transfer proof establishes conservation for successful and aborted transfers under nonnegative balances and transfer amounts, and the author judged the generated proof correct.On success, the source loses the amount added to the target; on failure, balances remain unchanged.Source: Assertion - the overall money in the… · p. 13

Human Prompt

• The scheduled-transfer implementation grew to 265 LOC, and the updated design's generated conservation proof was described as essentially the same as the one-time proof.The system adds a current time and a planned-transfer set, with transfers scheduled for later execution.Source: Human Prompt · p. 14

Generated proof

• The generated proof extends money conservation to scheduled transfers because each executes like a one-time transfer, while scheduling and advancing time do not change balances.It also argues that multiple transfers within a simulation stage preserve the total.Source: Generated proof · p. 15

A.3 Invariant coverage

• Coverage meant exercising relevant paths, not merely observing no violation, and required pre- and post-transfer checks plus success and failure cases for both transfer types.The stated criterion required both semantic cases at least once for one-time transfers and planned transfers.Source: Human Prompt · p. 15, §1 · pp. 15–16, §2 · p. 16
• Coverage also required cross-user and distinct-account transfers, planned-transfer insertion, persistence and execution, and a multi-transfer stage with checks after each operation.The planned-transfer lifecycle included insertion without balance changes, persistence across time steps, and execution at its scheduled time.Source: §3 · p. 16, §4 · p. 16, §5 · p. 16

Human Prompt

• Generated code achieved 100% of the specified runtime invariant-coverage conditions.The prompt asked the code to report coverage increases after each stage and the final percentage.Source: Human Prompt · p. 16

A.4 From natural to natural math to proof to code

• A later workflow explored asking for a minimal-mathematics natural-language description of the specification before proceeding through proof and code.The prompt requested the description as a LaTeX section.Source: §A.4 · p. 16, §A.4.1 · p. 16, Human Prompt · p. 16

Human Prompt

• The intuitive prompt describes user-owned accounts, a one-time transfer that succeeds only when the source has sufficient funds, and a simulation that selects inputs, executes, and reports the outcome.If funds are insufficient, the system makes no changes.Source: Human Prompt · p. 17

System Entities. Let

• The initial AI-generated specification had LaTeX errors and modeled a specific configuration rather than the general system, with additional correctness and balance-domain mistakes.The author identified that ownership correctness was left in English, balances were implicitly positive rather than non-negative, and zero transfers were allowed.Source: System Entities. Let · p. 19

General Mathematical Specification

• The revised general specification defines finite nonempty user and account sets, unique ownership as a partition, non-negative balances, and success or no-change transfer behavior.The prompt explicitly requested separation of the general specification from the simulation's specific configuration.Source: General Mathematical Specification · p. 20

Simulation-Specific Configuration

• The simulation instantiates the specification with three users, six accounts, fixed ownership pairs, randomly chosen initial balances, and randomly selected transfer inputs.The author reports that the generated description worked after prompting the AI to distinguish the specific simulation from the general specification.Source: Simulation-Specific Configuration · p. 21

Assertion - the overall money in the system is constant

• The proof establishes that total account balances remain constant for both successful transfers and rejected transfers.A successful transfer subtracts the amount from the source and adds it to the target; an insufficient-funds attempt leaves balances unchanged.Source: Assertion - the overall money in the… · pp. 21–22

A.4.2 Natural to natural math to proof when the natural specification is not complete

• The natural-language specification describes one-time transfers, and the author tests whether the AI detects an intentionally removed sufficient-funds check.The simulation randomly selects users, accounts, and an amount, executes the transfer, and reports the inputs and result.Source: §A.4.2 · p. 22

Specific Simulation Configuration The simulation uses

• The concrete simulation configuration uses three users and six accounts, with two accounts assigned to each user and randomly chosen initial balances.The general specification distinguishes this fixed simulation from arbitrary finite user and account sets.Source: §A.4.2 · p. 22, Specific Simulation Configuration The… · p. 23

General Specification

• The general specification models finite user and account sets, unique account ownership, account balances, and a transfer as a source, target, and amount.The operation requires its source and target accounts to belong to their specified users.Source: General Specification · pp. 22–23

Assertion - the overall money in the system is constant

• The stated assertion is that the sum of money across accounts remains constant after each transfer.The lemma passage identifies the claim as conservation of the total money in the system.Source: Assertion - the overall money in the… · p. 23

AI Reply

• The AI flagged that the injected lemma was ambiguous about summing balances, the transfer operation, nonnegative balances, and whether it applied to arbitrary account sets.It noted that conservation follows from algebraic cancellation whether or not transfers can overdraw, but rejected transfers must leave the state unchanged if overdrafts are disallowed.Source: AI Reply · p. 24

Lemma: Conservation of Total Money

• The total money in the system is preserved by a one-time transfer, even when insufficient-fund transfers are rejected without changing the state.The proof relies on offsetting the source deduction and target addition; fees, taxes, or money creation or destruction would require modifying the lemma.Source: Lemma: Conservation of Total Money · p. 24

A.4.3 From natural math to the Z formal specification notation

• The Z-style specification separates environment-selected inputs, state-changing successful and failed transfers, and observation of inputs and outcomes.Its explicit-environment formulation was judged cumbersome, prompting a second attempt using Z notation only for interfaces.Source: §A.4.3 · pp. 26–27

Human Prompt

• The revised human prompt uses Z schemas for one-time transfers, planned-transfer storage, scheduling, and execution, while retaining the surrounding natural-language specification.Each simulation stage advances time, attempts a random one-time transfer, schedules a future transfer, executes due transfers, and reports outcomes and planned-transfer state.Source: Human Prompt · pp. 27–28
• The revised specification explicitly states schema inputs and defines ExecutePlannedTransfers independently of a particular simulation configuration.It also specifies one-time transfers, planned-transfer scheduling and execution, and invokes either the successful or failure schema for a one-time transfer.Source: Human Prompt · pp. 29–31

Case 1: OneTimeTransfer. The schema defines

• The total balance invariant holds for every configuration reachable from a legal initial state through any finite sequence of the specified schemas.The induction covers successful and failed one-time transfers, planned-transfer scheduling, and execution; each schema preserves the sum of balances, so the result is independent of the simulation or execution strategy.Source: Human Prompt · p. 32, Case 1: OneTimeTransfer. The schema… · p. 33
• The AI identified the major interfaces, but mixed Z schemas with natural-language description, used a simulation-specific π6(p) reference, and omitted initialization details.The prompt asked it to add Z schema notation for interfaces while leaving the rest of the specification informal.Source: Human Prompt · pp. 33–34