runqiwang777/tracer 是面向 Lean 4 的 typed repair agent：它用编译器验证模型提出的证明候选，若验证失败，就利用错误诊断和相关示例尝试修复。仓库描述中还写有旧名称 runqi-allen-wang/TRACER-Typed-Repair-Agent-with-Compiler-validated-Example-Retrieval。仓库以 MIT 许可证公开，FACTS 中未记录最新发布版本。
README 记录的已完成试验，在 24 个问题和两种模型设置的重复条件下共涉及 864 个任务案例。其中 811/864（93.9%）在三次以内通过。仓库还包含重放这 24 个案例的功能，以及覆盖 254 个历史修复任务的基准测试。这说明它不只是生成证明候选的工具，而是依据编译结果反复迭代修复过程的工具。
不过，编译器反馈能提高成功率这一点尚未得到证实。README 的直接比较显示，使用反馈的结果在 Flash 上与无反馈重试的成功数相同，在 Pro 上则 72 个案例中少了两件。README 说明，更大规模的研究在公开结果之前，需要进行完整的追踪审计和独立的重新编译。因此，目前的结果更接近一份有待进一步验证的试验记录，而不是对可观性能的确认。