Hacker News 上有人用形式化方法给 coding agent 划重点，声称返工能明显降下来

Show HN：AxiomCode Graph，想给 coding agent 补上「改得对不对」这块盲区

Hacker News 这两天有个 Show HN 项目叫 AxiomCode Graph，作者 HaoleiZ 把仓库丢到了 GitHub（AxiomCodeAI/axiomcodegraph），帖子目前 10 分、8 条评论。表面上是早期工具的自我介绍，但评论区有人问了个在点子上的问题：你跟市面上那些给 agent 做代码图谱的东西，到底差在哪？

这问题值得展开，因为答案背后正好是 coding agent 现在绕不开的一块短板。不少代码图谱工具分析代码结构，靠的是 Tree-sitter、启发式规则或字符串搜索，也就是「能看懂语法树」，但对语义和依赖关系看得没那么细。AxiomCode Graph 走的是另一条路：用 DataLog 规则做形式化分析，而不是用 lean——作者原话是「lean 不是唯一路径」。他在回复里还给了个对比：在 Defects4J Benchmark 上达到 94.9% 的准确率，Graphify 是 48.7%。

这个数字不必急着全信，benchmark 只说明一部分问题，但它给了一个可复现的抓手，而不是空口说一句「我更懂代码」。真正值得留意的是它想解决的环节：工具把任意代码库转成一张「以形式化方法为地基」的知识图谱，给 coding agent 提供代码相关问题的精确回答，目的是让 agent 做出更完整、更正确的改动，同时减少返工、时间和 token 消耗。

这个切入点挺戳人。被 coding agent 反复返工折腾过的开发者都懂那种痛：agent 改完代码，你跑一遍测试，发现它漏了某个依赖调用，或者没考虑调用路径，又得让它回去改，来回一次就是白烧一轮 token 和时间。AxiomCode Graph 想解决的正是这中间的一环——让 agent 从一开始就有更完整的上下文，而不是靠跑测试碰运气才发现问题。评论区也有人直接表态，说只要真能降 token、提精度和效率，就没有理由不用。

它还有下一层规划，作者说很快会放出来：把工程规格和约束翻译成代码图谱之上的形式规则，用来验证 agent 生成的改动。这一步要是真做出来，就不只是「让 agent 少走弯路」，而是在改动落地前先校验它到底对不对，把返工的源头摁住。

说到底这还是刚放出来的 Show HN，属于早期阶段。准确率数字出自作者自己给的 benchmark，repo 也是新丢上来的，实际用起来稳不稳、扛不扛得住真实业务的复杂度，得等更多人把自家代码库喂进去才知道。作者自己也在评论区承认，整个行业才刚起步，他们只是尝试用一套可扩展的正式规则框架来做这件事，并不是想垄断这个方向。

不过这条线值得盯：把形式化方法搬进 coding agent 的工作流，方向站得住。它解决不了一切问题，但至少给「agent 到底改没改对」这件事，多了一个可验证的抓手，而不是全指望测试来回跑。眼下仓库已经可以看了，手头有正在被 agent 反复磨的代码库的，可以自己拉下来试一把。至于跑不跑得动、token 到底省没省、准确率有没有它说的那么高，得等你把真实代码喂进去才知道——这也是接下来要接受的检验。