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.
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
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.
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}
}More from The Secure Program Synthesis Hackathon
- View project: Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Vibe-Coding Specs: Eliciting, Editing, and Verifying Specifications for AI Coding Agents
Lida Safety
Specifications for real systems do not exist as one-shot artifacts: the user's intent emerges as they discover edge cases, rewrite drafts, and react to failing tests. We present an iterative pipeline that takes this …
- View project: AgentSpecGap
AgentSpecGap
solo-team
This prototype extracts rules from system prompts, tool descriptions, and runtime config. Rules are classified into one of interface validation, authorization check, workflow ordering validation, runtime validation, …
- View project: SpecGap Arena
SpecGap Arena
Obligation Cartographers
SpecGap Arena is a benchmark and framework that exposes how incomplete specifications let plausible but incorrect code pass public tests. It synthesizes missing semantic obligations (security boundaries, invariants, …