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가 밝힌다. 따라서 현재 결과는 유망한 성능의 확증이라기보다 추가 검증이 필요한 시험 기록에 가깝다.