Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 24, 2026India, United States

Proof Assistance as Verification Oracle for Porting

Abhinav Chand, Balaji R · Team Vajrapani

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

Read the report

Report: Proof Assistance as Verification Oracle for Porting

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

This project tests a formal-verification harness on Anthropic’s Bun rewrite work, where AI-generated Rust ports are checked against their original Zig implementations. The harness translates Rust into Dafny, extracts behavioral theorems from Zig, and attempts to prove those theorems against the Rust-derived model. In practice, this produced real verifier failures that exposed real bugs, showing that proof-driven auditing can help make AI-generated software ports more trustworthy.

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. Thank you for this great work. Very impressed by the real-world results of two bugs reported (and merged!) in the production code (!!) of a major open-source project.

    Super-relevant for oh-so-common software replattforming projects.

    I'd recommend including specific examples from your experiment runs in the results section, and potentially some stats on theorems derived, proof successes / failures, etc, to illustrate the process.

    The discussion section mentions the alignment problem, which in general is relevant, but does not tie into the rest of your write-up from what I can see.

  2. By far my favorite among the projects I reviewed. Thanks for a well-thought-out tool constructed quickly!

    The interesting thing about this project is, as its title alludes to, using relatively heavyweight formal-methods tooling to augment what is really just systematic testing, in that no formal guarantee of correctness follows, but we may nonetheless find bugs missed by more-traditional testing. Indeed, the handful of real bugs reported against Bun is the high point of this project, showing genuine impact.

    I do still see something of a Frankenstein's-monster flavor to the project. The translation into Dafny is somewhat arbitrary; using a native Rust verification tool makes more sense, though probably those tools aren't as mature as Dafny. Perhaps more importantly, the translation is done with Claude Code, which adds further "buyer beware" cautions that shouldn't leave us with particularly more confidence than just asking Claude Code to audit the Rust code directly.

    The approach also depends on asking Claude Code to audit Zig code and identify properties worth preserving into Rust. I don't have high confidence that such a process will be very comprehensive. However, the authors found real bugs, so they should get credit for demonstrating genuine utility.

    Read full reviewShow less

Cite this project

@misc{chand2026proof,
  title = {{Proof Assistance as Verification Oracle for Porting}},
  author = {Abhinav Chand and Balaji R},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/proof-assistance-as-verification-oracle-for-porting-ma88}},
  url = {https://apartresearch.com/sprints/projects/proof-assistance-as-verification-oracle-for-porting-ma88}
}

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