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

• URL: http://arxiv.org/abs/2609.07365v1
• Date: Mon, 07 Sep 2026 11:35:49 GMT
• Title: Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking
• Abstract summary: Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice.<n>We argue that AI can serve as an intermediate specification language that is precise enough to reason over and prove.<n>The specification becomes the artifact one authors, reviews, proves, and refines; the code becomes regenerable output.
• Score: 1.6796354350132203
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice. We argue that AI removes much of that cost: natural language enriched with lightweight mathematics, written in \LaTeX, can serve as an intermediate specification language that is precise enough to reason over and prove, while a large language model (LLM) reviews it for ambiguity, drafts proofs, and generates the implementation. The specification becomes the artifact one authors, reviews, proves, and refines; the code becomes regenerable output. This paper is a follow-on to a prior study that established the discipline on an organizational-knowledge-growth simulation~\cite{predecessor2026}. Here we replicate the discipline in a different domain---an online-banking fund-transfer service---and extend it. The two domains share one spine: a conservation invariant (knowledge in the prior study, money here), which suggests the approach generalizes across domains. We contribute: (i) a second, independent case study of the method; (ii) a stress-test of the method on a richer problem---\emph{scheduled/recurring} transfers---whose generated code grows substantially while the invariant and its proof do not; (iii) an \emph{AI-proposed runtime coverage model} for invariants (``never violated $\neq$ covered''); and (iv) a Z formalization, including paired success/failure operation schemas and an invariant proved over the inductive set of all reachable configurations, together with an experiment in which the AI proposes the Z interfaces itself. We are explicit about the method's limits: the proofs and runtime checks live at the specification level and do not establish that the generated code refines the specification---that step is delegated to the AI. This is a case study, not a controlled experiment.

Related papers

• Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning [0.0]
  Eigenius is a knowledge-graph built on a single premise: answering the audit question "what do you know and what is your warranty?"<n>It turns data proofs into a structural invariant rather than a property reconstructed across subsystem boundaries.
  arXiv  Detail & Related papers  (2026-08-05T05:28:22Z)
• A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
  We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game.<n>The objective is to turn a document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone.<n>The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route.
  arXiv  Detail & Related papers  (2026-07-09T23:17:54Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• The Deterministic Horizon: Impossibility Results as Design Specifications for Trustworthy AI Systems [0.0]
  This thesis turns impossibility results from curiosities into design rules.<n>Its flagship result proves an accuracy ceiling set by architecture alone.<n>The same argument recasts across subfields.
  arXiv  Detail & Related papers  (2026-05-21T20:48:35Z)
• DPrivBench: Benchmarking LLMs' Reasoning for Differential Privacy [50.73304874527716]
  Differential privacy (DP) has a wide range of applications for protecting data privacy, but designing and verifying DP algorithms requires expert-level reasoning.<n>We introduce DPrivBench, a benchmark in which each instance asks whether a function or algorithm satisfies a stated DP guarantee.<n>Experiments show that while the strongest models handle textbook mechanisms well, all models struggle with advanced algorithms.
  arXiv  Detail & Related papers  (2026-04-17T09:03:11Z)
• The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
  The dominant industry response to AI-generated code quality problems is to deploy AI reviewers.<n>This paper argues that this response is structurally circular when executable specifications are absent.
  arXiv  Detail & Related papers  (2026-03-26T11:59:05Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  We conduct a user study involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages.<n>Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process.<n>We translate these findings into concrete design guidance for AI proof assistants.
  arXiv  Detail & Related papers  (2025-08-01T22:16:30Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.