信任规范，而非代码——在线银行中规范优先、AI辅助的案例研究

中文摘要 AI 辅助

形式化规范承诺早期错误检测、显式不变量和设计正确性，但其符号成本使其未能进入主流实践。我们认为AI消除了大部分成本：用LaTeX编写的、以轻量数学增强的自然语言，可以作为中间规范语言，足够精确以进行推理和证明，同时大型语言模型（LLM）审查其歧义、起草证明并生成实现。规范成为作者编写、审查、证明和完善的工件；代码成为可再生的输出。本文是先前研究的后续，该研究在组织知识增长模拟中确立了这一方法。在此，我们在不同领域——在线银行资金转账服务——复制该方法并加以扩展。两个领域共享一条主线：守恒不变量（先前研究中的知识，此处为金钱），这表明该方法可跨领域推广。我们的贡献包括：（i）该方法的第二个独立案例研究；（ii）在更丰富的问题上对该方法进行压力测试——\textit{计划/定期}转账——其生成代码大幅增长，而不变量及其证明并未增长；（iii）AI提出的不变量运行时覆盖模型（“从未违反$\ eq$已覆盖”）；（iv）Z形式化，包括成对的成功/失败操作模式和一个在可达配置归纳集上证明的不变量，以及一个AI自行提出Z接口的实验。我们明确说明方法的局限性：证明和运行时检查位于规范层面，并未确立生成代码精化规范——该步骤委托给AI。这是一个案例研究，而非受控实验。

英文摘要

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.

发表机构

• IBM Research（IBM研究院）

机构由 AI 辅助整理，请以论文原文为准。