Apple和Goldman把成千上万条争议弄丢进了一个无人知晓的状态，代价是8900万美元。
2020年6月，Apple在Apple Card的争议处理流程中新增了一个表单。一件小事。在此变更之前，你点击"报告问题"，进入一个与Goldman Sachs的Messages对话，你的争议申请就此提交。而在变更之后，你在完成第一次提交后，还必须再填写第二个表单。
这件小事造成了如下后果。如果你在Messages中报告了问题，却从未完成第二个表单，系统就会判定你的争议申请不完整。它从未被发送给Goldman。没有人对它展开调查。也从未发出过任何确认函。而根据Regulation Z第1026.13节，那些最初的消息中有很多是有效的账单错误通知——按法律规定，债权人必须在30天内予以确认，并在两个账单周期内予以解决。
成千上万条这样的争议就那么搁置着。已提交，却无处流转。2024年10月，消费者金融保护局（CFPB）责令Apple和Goldman Sachs为此支付8900万美元，并禁止Goldman在没有可信合规方案的情况下推出新信用卡。我职业生涯中有很长一段时间都在一家发卡机构的争议处理运营部门度过，当我读到那份处罚令时，我看到的不是疏忽。我看到的是一台带有漏洞的状态机，而据我所知，每一家银行如今在自己的工作流程中某处都有这样一个漏洞。
这就是我在本文中想让你相信的事：你的争议处理系统里有一些你尚未发现的死状态，而你之所以没有发现它们，是因为你一直在为它们做测试，而不是证明它们不可能存在。解决之道是一项大多数银行从业者从未被提供过的技术——形式化验证——这也正是我们围绕它构建了Veriprajna的金融合规验证实践的原因。
那个8900万美元的漏洞是一种状态，而非一个失误
让我精确地说明究竟出了什么问题，因为这份精确正是全部要点所在。
Apple-Goldman的工作流程中有一个可达状态，你可以用一句话描述它：这项争议处于FormA_Submitted AND FormB_Pending。从这个状态出发，没有任何通向Investigation_Initiated的转换。一个都没有。一个在发送第一条消息后就停下来的消费者，会永远停留在那里——按法律应得到确认，按系统自身的逻辑却什么都得不到。
这些争议并没有丢失。它们恰恰就在系统所放置的地方。只是系统从未被告知，"这里"是一个争议可能会消亡的地方。
当我的团队第一次在白板上梳理这件事时，一位工程师说了句显而易见的话——这只不过是个漏洞，是我们在测试中本该抓到的那种。我问他怎么抓。Apple-Goldman的流程只有一个两套系统之间的集成点。而我共事过的大多数大型发卡机构，都有10到15套系统在触及单一一项争议——Visa VROL门户、Mastercard的GCMS、案件管理平台、核心银行账务系统、函件生成系统、征信机构数据馈送、临时授信引擎，以及一大把内部路由队列。每一次API变更、每一次合作方集成、每一项新的产品功能，都会在那座迷宫中开辟出新的路径。
测试所检验的，是你想到要写下来的那些路径。按定义，它就是一份你已经设想过的失败清单。Apple-Goldman那个死状态是一个无人设想过的失败，而这恰恰是没有任何测试覆盖它的原因。你无法通过测试摆脱一个你根本无法想象的问题。这不是流程上的失败。这是一道数学上的天花板。
我们为什么不能直接多写些测试？
我曾为这场争论耗掉了一个下午，所以让我替你省下这个下午。
那位工程师的反驳是合情合理的：多写些测试用例。覆盖更多路径。把覆盖率提上去。于是我把它画了出来。一个争议处理工作流程不是一条线，而是一张图——按争议类型分支，按网络分支，按是否发放了临时授信分支，按适用哪套时限制度分支，按合作方系统是否确认了交接分支。每一个分支都在成倍放大上一个。一个有几十个决策点的工作流程，其可达状态之多远超你所能写出的测试数量，而那些危险的状态，正是无人坐下来逐一列举的组合，因为在它们发生之前，它们看上去都荒谬至极。
他又坚持了一会儿。然后我画出了组合爆炸——状态数量翻倍，然后再翻倍——他就停下了。你无法用测试战胜一个状态空间。你会在耗尽状态之前先耗尽你手里的硬币。
就是在这一刻，我开始认真研读形式化方法，而这里关键的那项技术有一个朴素的描述。一个模型检查器接受你工作流程的一个模型，以及一个不变式——一条必须始终成立的性质——然后它会详尽地探索每一个可达状态，寻找一个使该性质被打破的状态。把不变式写成"每一项已提交的争议都在30天内到达确认"，让检查器对准Apple-Goldman的流程，它就会在几秒钟内返回那个死状态，连同把你带到那里的确切逐步路径。像TLA+这样的工具为分布式系统做这件事；同样的逻辑可以干净利落地应用于一个带有硬性时限的受监管工作流程。
测试对你想象过的路径进行抽样。模型检查器则去访问那些你没想象过的路径。
无人负责的时间线冲突
真正让争议处理主管夜不能寐的那部分，比单单一个死状态更糟。
单单一项双网络卡片争议，就可能同时触发三四个监管和网络时钟。Reg Z要求在30天内出具书面确认，并在两个账单周期内解决，上限为90天。Reg E——它规范借记与电子转账错误——则运行在一套完全不同的时间表上：临时授信和解决须在10个营业日之内完成，另有45个日历日的延展期。Visa Claims Resolution对Allocation类案件的处理期限最长为70天，对Collaboration类案件最长为100天。Mastercard的争议框架视周期不同运行45到120天，而业界形容其推行过程比Visa的更难消化。
当这些制度在同一项争议上相撞时，合规与否就取决于争议处理台上那天上午谁记得该由哪条时限主管。我曾眼看着一位资深分析师把Reg E的时限套用到一项Reg Z的账单错误上，因为在业务量之下两者会相互模糊——而这种确切的混淆，正是CFPB审查官会去查找的违规之一。Citizens Bank部分正是因为以缺少一份宣誓书为由拒绝账单错误通知而被点名。这些时限并不软性。它们是二元的。你要么在30天内做了确认，要么没有。
而这就是形式化验证契合金融合规的那个安静的理由——契合程度胜过我所能想到的几乎任何其他领域：这些规则本身就已经是数学。30天不是一个可自由裁量的判断。"10个营业日内的临时授信"不是一种感觉。这些是施加在状态机之上的时序约束，而时序逻辑正是为证明这类性质而生的——即在一项争议所能走的每一条可能路径上，没有任何一个时钟被冲破。
我最先造错了东西
我想跟你讲讲我们发布出去却行不通的那个版本，因为市场上大部分人至今仍在售卖的正是这个版本。
我们最初的直觉是监控。造一套系统，追踪每一项争议，盯着各个时限，当某一项即将超期时就亮起红灯。仪表盘。告警。一个临时授信队列在倒计时——9天，23小时，走。它演示起来相当漂亮。我曾为它感到自豪。
然后我把它拿给一家试点银行的合规主管看，她只是礼貌地耸了耸肩。我花了几天才理解那个耸肩。一个监控器在一项争议消亡的同时告诉你它正在消亡。它是个烟雾报警器。它假定这项争议一开始就进入了系统、可供追踪——而这恰恰是Apple-Goldman击碎的那一个假定，因为那些争议根本从未被追踪；它们处于一个追踪器不知道要去盯的状态。监控是事后的忏悔。它是让银行比审查官稍早一点发现自己的失败。这有一定价值，但那不是她需要摆到董事会面前的东西。
监控为你争取到的，是比审查官早几天发现失败。它永远无法为你换来那个不可能发生的失败。
那个耸肩让我们付出了一次重建的代价，而它是这个产品所遇到的最好的事。市场上充斥着我最先造出来的那种东西。FINBOA追踪Reg E的时限并将临时授信自动化；它在这方面做得不错。Quavo将争议处理自动化并交出真实数据——某家信用合作社在一个月内达到了87%的自动化率。FIS通过各网络门户处理拒付。它们中的每一个都在自动化或盯守那些已经进入系统的争议。它们中没有一个能证明，一项争议在进入系统之前不会丢失。
还有谁真的在证明任何东西？
在那次重建之后，我去寻找还有谁在证明事物、而非盯守它们，答案是几乎没有人。
唯一一个认真的名字是Imandra。他们在金融服务领域做真正的形式化验证——对正确性的数学证明——他们的客户就包括Goldman Sachs本身。但他们的世界是资本市场：交易所撮合逻辑、交易协议。消费者合规、Reg Z、争议处理工作流程——那不是他们所瞄准的方向，而且在总共约500万美元的融资规模下，他们也没有瞄准那里。
与此同时，资本正涌入合规领域另一个角落。Bretton AI——其前身为Greenlite——筹得了一轮7500万美元的B轮融资，时间是2026年2月，服务对象是受OCC监管的银行——用于KYC、反洗钱和客户引入。SymphonyAI的Sensa平台把某家西班牙银行制裁筛查中的误报率削减了91.8%。Alloy在800多家机构之间编排身份识别。真金白银，真材实料的工程——但全都瞄准金融犯罪与客户引入，没有一分是瞄准你的争议解决是否可能违反某项法规。
这就是那道缺口，而它并不狭窄。最接近争议处理工作的玩家（FINBOA、Quavo）将其自动化，却不验证它。唯一的验证者（Imandra）耕耘的是另一个市场。把这两者合起来，你就得到这一领域的一个角落——就我所能看到的，还没有人站在里面：对准消费者争议合规的形式化验证。那个角落正是我们走进去的地方。
那句重建了我们推介的话
最终让这份价值在我心中落地的那样东西，并非来自一位工程师。它来自我坐下来交谈过的一位前审查官。
我问她，在一场账单错误审查中，她在场时真正想要的是什么。她没有说"好的仪表盘"。她大致是说，她想要知道这家银行能够证明它的流程不可能错过时限——而不是它通常没有错过。整个姿态就系于那一个词而翻转。那张写着"我们测试过了，通过了"的董事会证明幻灯片，是一份承认：你只检查了你想到的那些路径。而一份证明所陈述的东西在类别上更为强大：在这个工作流程所允许的每一条路径上，不变式都成立。
而监管机构也在悄悄地、靠他们自己朝这个方向走去。OCC Bulletin 2025-26明确了：任何实质性驱动某项风险或合规决策的定量方法都是一个"模型"——而该公告明确指出，AI或机器学习的复杂精巧并不能使其豁免于验证。仔细读这一点：一个自动化的争议路由器如今作为一个模型、而不仅仅作为一件运营工具，是可被审查的。而形式化验证是现存最强的模型验证。它不对行为进行抽样。它证明性质。
在大西洋彼岸，《欧盟人工智能法案》（EU AI Act）将信贷及信用评估类AI归类为高风险，设有一个硬性合规截止日期——2026年8月2日——并具有域外效力，把服务于欧盟市场的美国供应商也纳入其中。高风险归类意味着你必须展示系统可被证明的性质——准确性、稳健性、监督。这再一次，正是一份证明所能交付、而一次测试无法交付的东西。
这对一个争议队列来说不是杀鸡用牛刀吗？
人们不断以各种版本向我提出这个问题，所以让我正面迎击这三个诚实的反对意见。
第一个是成本。验证听起来像一个科研项目，而咨询这条替代路径——一家四大会计师事务所替你重新设计流程——要花费50万美元到几百万美元，交到你手里的是一套没有人在数学上检查过的重新设计的流程。把它和不利后果放在一起衡量。Apple-Goldman是8900万美元。Wells Fargo的同意令，横跨包括争议处理在内的多项失败，高达37亿美元。你买验证，不是拿它去对冲一份SaaS许可证的成本；你买它，是拿它去对冲那条尾部风险。
第二个是"我们的业务量没问题"。全球拒付预计到2026年将达到每年3.37亿笔，并在2028年之前攀升24%，其间还会出现全新的争议类型——包括来自自主AI代理购买了客户从未批准的东西而引发的争议。今天"应付得来"的那个人工处理台，正是那个仍有42%的机构在人工流程上运行合规的处理台，这一数据出自Wolters Kluwer的2026年第一季度报告。业务量上升，加上依赖人工记忆，正是一个死状态得以四年无人察觉的方式。
第三个是"我们通过了上一次审查"。想必Apple和Goldman也通过了，一直到他们没通过的那一刻。通过一次审查，意味着一位审查官抽样查看了你的路径，而没有撞上那条坏掉的。这和测试是同一个抽样问题，只是佩戴着一枚不同的徽章。
我如今所相信的
我走进争议处理运营时，以为合规是一门关于勤勉的功课——细心的人、好的清单、按时达成的时限。走出来时，我确信勤勉对于这般形状的问题而言是一件用错了的工具。你不可能勤勉到足以覆盖一个每次有人发布功能就翻倍的状态空间。Apple和Goldman那些细心的人并不是因为粗心而丢失了那些争议。他们丢失它们，是因为一个无人画出的状态。
所以，我想对任何经营着一个争议处理台的人提出的问题，不是"你们的人细不细心"。它比那更狭窄、更冷峻：你能画出你下一项被丢弃的争议将会消亡于其中的那个状态吗？如果你画不出它，你就无法为它测试；而如果你无法为它测试，剩下唯一诚实的事，就是证明它不可能存在。这就是那份工作——在审查官找到你漏掉的那一条之前，证明你的争议处理工作流程在每一条路径上都不可能违反Reg Z、Reg E以及各网络时限。如果这正是你真正需要的那份保证，那正是我们所构建的东西。
Apple有成千上万名工程师，却仍然有一个死状态。工程师从来都不是那个缺失的变量。一份证明才是。
