Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Overland Park

ITP Fuzz

Pruthviraj Sadhankar · Team Fuzzers

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: ITP Fuzz

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

A framework for finding failure modes in interactive theorem provers (ITPs) and LLM-assisted proof tools.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. The document outlines the problem but fails to propose a solution or methodology. Furthermore, the linked repository does not contain any code.

  2. itp-fuzz presents a compelling framework for adversarial robustness testing of interactive theorem provers (ITPs) and LLM-assisted proof tools. The project successfully identifies and categorizes failure modes through kernel fuzzing and AI assistant testing, which are critical areas in ensuring the security and reliability of these systems. The kernel fuzzing method, particularly its ability to detect configurations that disable essential checks like setting 'debug.skipKernelTC' to true in Lean, demonstrates a practical approach to uncovering vulnerabilities. Additionally, the AI assistant testing component is innovative for its focus on tricking LLM-based autocompleters into suggesting unsafe tactics, which is a novel and important angle in the context of program synthesis security.

    However, the project could benefit from more comprehensive validation across different ITPs and LLM configurations to ensure broader applicability. While the Coq interface is successfully integrated, the framework's effectiveness on other systems like Lean, Isabelle, and F* remains somewhat speculative without extensive testing results. The living vulnerability database is a valuable resource, but it lacks detailed analysis of the discovered vulnerabilities, which would provide deeper insights into their potential impact and mitigation strategies.

    To enhance the project’s impact and robustness, future work should include a more thorough cross-platform evaluation to establish the framework's reliability across various ITPs and LLM environments. Additionally, expanding the vulnerability database with detailed case studies and mitigation techniques could significantly improve its utility for both researchers and practitioners. Despite these limitations, itp-fuzz demonstrates a strong foundation in addressing critical security issues in formal verification systems, making it a promising tool for advancing the field.

    Also, There is no code present on GitHub. The Paper does contain the verification commands.

    Read full reviewShow less

Cite this project

@misc{sadhankar2026itp,
  title = {{ITP Fuzz}},
  author = {Pruthviraj Sadhankar},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/itp-fuzz-irn7}},
  url = {https://apartresearch.com/sprints/projects/itp-fuzz-irn7}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026