Skip to content
Sprint projectMay 25, 2026Paris, France

RAFT: Gradual Typing, Invariance Enforcement, and Property Verification in Research Python.

Thomas Winninger, Antonin Peronnet · Team RAFT

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

Read the report

Report: RAFT: Gradual Typing, Invariance Enforcement, and Property Verification in Research Python.

Recording (opens in new tab)
Share

AI researchers prototype in short scripts or Jupyter notebooks and push directly to state-of-the-art frameworks like `transformers` or `vLLM`. They lack the time for rigorous testing or manual verification. Moreover, the nature of their work makes traditional test or spec-driven development difficult to apply. We propose an automated, iterative pipeline to bridge the gap between quick experimental scripts and shareable, verifiable code, utilizing AI and strict static analysis to gradually introduce typing, contracts, and property verification. We validate our results with a backdoor detection experiment. A small reviewer `gemma4 e4b` is more efficient at finding bugs and backdoors after the application of our method. Going from 46% recall on vanilla code, to 95% detection on the `transformers`'s library.

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 paper highlights a real problem which is turning ad‑hoc research code into verifiable artifacts and the ablation study is thoughtfully designed. That being said, the core contribution feels limited, as RAFT mainly orchestrates existing static analysis tools rather than introducing new techniques. The large reported gain in backdoor detection appears driven mostly by a prompting change, not by code transformation itself. Evaluating on only seven repositories with a small, quantized model limits confidence in the results; testing on larger codebases and stronger models would make the claims more convincing.

  2. Gradual typing is a strong idea for secure program synthesis -- it allows rapid code development to be moved towards guarantees. This sprint covers two directions: a tool chain called rafty, built of various gradual typing related tools, and a new tool called annassert, which converts python asserts into type annotations that can then be checked by other tools as compile time. Going forward I'd be curious about how much typical python code is in the format that annassert suggests; this could be checked by running over the samples in the repo or more broadly some chunk of repos from github.

Cite this project

@misc{winninger2026raft,
  title = {{RAFT: Gradual Typing, Invariance Enforcement, and Property Verification in Research Python.}},
  author = {Thomas Winninger and Antonin Peronnet},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/raft-gradual-typing-invariance-enforcement-and-property-verification-in-research-python-pcns}},
  url = {https://apartresearch.com/sprints/projects/raft-gradual-typing-invariance-enforcement-and-property-verification-in-research-python-pcns}
}

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026