Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 24, 2026Cape Town

Axiom Zero: AlphaZero-Style Reinforcement Learning for Automated Formal Verification of Python Programs

Mufaro Rukuni, Brain Monzora · Team Axiom_Zer0

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

Read the report

Report: Axiom Zero: AlphaZero-Style Reinforcement Learning for Automated Formal Verification of Python Programs

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

The rapid growth of AI-generated code has created a verification crisis: Gross World Lines of Code (LoC) is expanding at unprecedented rates, yet developers have no systematic guarantee that the code produced by large language models behaves as intended. We present Axiom Zero, a compiler and reinforcement learning system that translates Python/PyTorch source code into formal proofs verified by the Lean 4 proof assistant, using an AlphaZero-style agent to discover those proofs automatically without human-labelled examples. The system comprises four implemented phases: (1) a parse pipeline that converts Python source into a normalized intermediate representation with type and tensor-shape analysis; (2) a proof environment modelling theorem proving as a two-player game with 39 curated tactics across 10 categories; (3) a policy-plus-value network with MCTS tree search trained via self-play; and (4) a Python-to-Lean 4 compiler with difficulty-stratified proof-hole filling. All 143 unit tests pass across 3,450 lines of dependency-free Python. The Lean 4 kernel serves as the binary oracle: a proof either compiles or it does not, providing a clean reward signal that eliminates the need for human annotation. Axiom Zero demonstrates that the game-theoretic self-play paradigm, previously applied to chess and Go, can be transferred to the domain of program verification, offering a scalable path toward trustworthy AI-assisted software development.

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 write-up for this project was clear, well-polished communication. I would be very interested to see the results of Phase 5, which are ongoing. The 3.5 design decisions all seemed appropriate and improved usability. The test suite had good, relevant and broad coverage.

    I was not convinced by claim of 'isomorphism' or even substantial similarity to superhuman Go via self-play - the prover and kernel do not coevolve, and this approach is more aptly described as an expert iteration / single-agent search method.

    I think limiting it to Lean 4 is basically fine.

  2. This is a very ambitious project and it's great to see the authors got very far! A larger evaluation with more test cases would be useful next -- and, ideally, the authors would verify the correctness of their translation steps.

Cite this project

@misc{rukuni2026axiom,
  title = {{Axiom Zero: AlphaZero-Style Reinforcement Learning for Automated Formal Verification of Python Programs}},
  author = {Mufaro Rukuni and Brain Monzora},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/axiom-zero-alphazerostyle-reinforcement-learning-for-automated-formal-verification-of-python-programs-aqr7}},
  url = {https://apartresearch.com/sprints/projects/axiom-zero-alphazerostyle-reinforcement-learning-for-automated-formal-verification-of-python-programs-aqr7}
}

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