用途：这是一套定向形式化 bug 排查方法，而非全程序验证。它只对代码库中风险较高的切片建模，用来发现测试难以覆盖的交错场景，例如双写无锁、非幂等重试、取消与成功路径竞态、至少一次投递无去重、带过期的锁或租约、回调先于被引用对象到达、多值状态列、以及可能重复执行的同步/重放/回填等。
流程（须按序执行）：1）先廉价地勘察仓库，列出3–6个疑似竞态或有状态的子系统，说明文件、非正式状态机、并发点和风险理由，再选定最高价值目标并等待确认；2）阅读实现、测试、注释与调用点，写出英文规格，记录歧义而非猜测；3）按问题形态选工具：单一状态机与不变式用 Lean 4，交错、竞态、重试、取消、并发写用 TLA+ / PlusCal，纯函数的代数性质用 Lean 4。模型要小且忠实，每个转移标注 file:line，无法证明处用 sorry 并说明假设，模型放在 formal/ 或 spec/ 下每目标一个目录并附 README；语法与安装见 references/lean.md 和 references/tlaplus.md；4）寻找反例（双发、丢取消、卡住重试、陈旧读、非法状态转移、丢错误、重入、超时与成功竞态、丢失更新、已删状态复活）；5）在真实代码上复现，转成失败测试或确定性复现脚本，分类严重程度与受影响范围，无法复现则记录为未复现嫌疑而不改代码；6）做最小正确修复，补上先失败后通过的测试，若模型揭示更简单设计则作为独立后续提案；7）按发现报告标题、所用模型、被违反性质、复现、根因（file:line）、补丁、新增测试、残余风险与未证假设，并列出发现数、未复现嫌疑与下一个目标。
限制与安全：不得声称整个仓库已验证，只说明建模了什么、没建模什么。不得写入生产数据库，不得自行查询生产数据，反例须对代码与测试验证而非对线上行验证；模型提出的 schema 变更只是提案。不要大规模重写代码库，不要静默改变预期行为，修复按仓库常规方式落地。当已有可靠复现、逻辑为直线型无并发无状态机、答案只是类型改动或空值检查、或无人维护规格时，不应使用本方法。写入模型便宜，证明昂贵，应先做状态探索（TLC、Lean 的 #eval/decide）再考虑证明。
费用、许可、平台支持等资料暂未提供。