runqiwang777/tracer は Lean 4 向けの typed repair agent であり、モデルが提案した証明候補をコンパイラで検証し、失敗した場合はエラーダイアグNOSティクスと関連事例を活用して修正を試みる。リポジトリの説明には、旧名称である runqi-allen-wang/TRACER-Typed-Repair-Agent-with-Compiler-validated-Example-Retrieval も記載されている。MIT ライセンスで公開されており、FACTS に記録された最新リリースはない。
README が記す完了済みの試験では、24 問と 2 つのモデル設定での反復条件のもとで 864 件の試行事例を対象とする。3 回以内に合格した事例は 811/864 件（93.9%）である。リポジトリには、その 24 事例を再生する機能と、254 件の過去の修復課題に対するベンチマークも含まれている。これは、証明候補を生成するにとどまらず、コンパイラの結果に基づいて修正の過程を繰り返すツールであることを示している。
ただし、コンパイラのフィードバックが成功率を高めることは実証されていない。README の直接比較では、フィードバック使用時の結果は Flash ではフィードバックなしの再試行と成功数が同じで、Pro では 72 事例中 2 件少なかった。README は、より大規模な研究では結果を公開する前に完全なトレース監査と独立した再コンパイルが必要だと述べている。したがって現状の結果は、有望な性能の確証というより、追加の検証を要する試験記録に近い。