AI for Verified Software

We aim to build AI systems that produce software with machine-checkable guarantees and make formal verification a routine part of software development.

Related publications

2026

  1. Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
    Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
    Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, and 6 more authors
    arXiv, 2026
    Code
  2. Propose, Solve, Verify: Self-Play Through Formal Verification
    Propose, Solve, Verify: Self-Play Through Formal Verification
    Alex Wilf, Pranjal Aggarwal, Bryan Parno, and 4 more authors
    2026
    ICML 2026
    Code

2025

  1. AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

2024

  1. miniCodeProps: a Minimal Benchmark for Proving Code Properties
    miniCodeProps: a Minimal Benchmark for Proving Code Properties
    E. Lohn, and Sean Welleck
    2024
    NeurIPS 2024 Workshop on Safe Generative AI