InvGen 开源：用 LLM 生成 C 程序循环不变式、CBMC 与 Frama-C 验证

InvGen 是一个开源工具，用 LLM 为 C 程序生成循环不变式，再由符号工具验证：LLM 可走 Claude Code CLI（订阅登录，无需 API token）或经 Ollama 跑本地模型如 qwen3:8b，候选不变式由 CBMC 做 BMC 过滤并执行 Houdini 归纳子集筛选，最终由 Frama-C/WP 完成正确性证明。每次失败的检查会转成带具体状态的反例句子追加进提示词，仓库还提供 compare.py 在相同 K/m 参数下对比不同模型，附带 Code2Inv 全集 133 个线性与 7 个非线性程序（其中 9 个断言有错，可被 BMC 查出），代码约 1300 行。