VeriCodeGen: AI for Verifiable Coding

Description

LLM code assistants today are powerful but fundamentally untrustworthy: they hallucinate logic, mis-handle corner cases, and provide no guarantees. This workshop centers a different goal: AI for Verifiable Coding, where human-aligned agents collaborate with proof assistants, model checkers, SAT/SMT solvers, and static analyzers to co-design specifications, code, proofs, and heuristics with machine-checkable guarantees.

We argue that such agents must be built very differently from generic code LLMs. Verifiable generation requires rich specification languages (from contracts and types to temporal logics and proof terms), symbolic backends, and structured interaction loops where models propose artifacts and tools refute, repair, or certify them. Beyond code (Lean, Rust/Verus, Coq, Isabelle, Dafny, etc.), these agents must support autoformalization of informal requirements and mathematics, proof search for complex verification conditions, and heuristic discovery, e.g., invariants, lemma libraries, and solver strategies, that amplify classical formal-methods tools.

We will highlight opportunities and hard problems unique to this setting: aligning learned models with human intent expressed as specifications and proofs; orchestrating multi-agent toolchains that mix neural search with symbolic reasoning; scaling autoformalization beyond toy examples; designing training signals from compiler, verifier, or theorem-prover feedback; and building evaluation protocols that track end-to-end guarantees, not just pass@k. The goal is a roadmap toward collaborative agents that help humans understand, control, and verify the software and systems they generate.

Call for Paper Topics

This workshop brings together researchers in LLMs, formal methods, programming languages, and HCI to discuss questions including (but not limited to):

Neuro-symbolic architectures: LLM agents integrated with proof assistants, model checkers, solvers, static analyzers, and compiler feedback; verifier-guided training and inference.
Specification generation and quality: autoformalization, specification mining, ambiguity and inconsistency detection, property-based validation, and human-guided refinement.
Proof search and engineering: premise selection, tactic learning, proof repair, maintenance, scalability, and compatibility across theorem-proving systems.
Program verification and repair: deductive verification, model checking, symbolic execution, abstract interpretation, testing, debugging, certified repair, equivalence checking, and behavior preservation.
Verification applications: security, smart contracts, memory safety, supply chains, access-control policies, network configurations, infrastructure-as-code, and distributed protocols.
Verification of and for AI: formal validation of generated outputs, runtime monitoring of agents, verified guardrails, and constrained tool use.
Solver and trusted infrastructure: scalable SAT/SMT solving, learned heuristics, proof certificates, independent checking, trusted computing bases, and verifier validation.
Human-centered verification: mixed-initiative interfaces, explanations, trust calibration, and accessibility for developers without formal-methods expertise.
Benchmarks and deployment: datasets and metrics for end-to-end guarantees, scalability studies, reproducibility, negative results, and industrial experience.

Confirmed Speakers / Panelists (A-Z by Last Name)

Leonardo de Moura

Senior Principal Applied Scientist, Automated Reasoning Group, Amazon Web Services

Emily First

Assistant Professor, Rutgers University (New Brunswick)

Vijay Ganesh

Professor, Georgia Institute of Technology

Patrick Li

Harmonic

Shan Lu

Professor, University of Chicago

Baishakhi Ray

Associate Professor, Columbia University

Bartley Richardson

CrowdStrike

Shubho Sengupta

CTO, Axiom Math

Patrick Shafto

DARPA & Rutgers University

Dawn Song

Professor, University of California, Berkeley

Call for Papers (Research Paper Track)

We provide more submission details: Guidance for VeriCodeGen CFP at NeurIPS 2026.
OpenReview submission portal: https://openreview.net/group?id=NeurIPS.cc/2026/Workshop/VERICODGEN
Paper format: Prepare your paper with neurips_2026_vericode_workshop.tex and neurips_2026_vericode.sty, both in the Overleaf project.

Tentative important dates (AoE time):

Abstract Submission Deadline: September 11, 2026
Paper Submission Deadline: September 13, 2026
Review Deadline: September 27, 2026
Acceptance/Rejection Notification Date: September 29, 2026
Import Accepted Papers: October 4, 2026
Camera-Ready Submission: October 14, 2026
Workshop Date: December 12 (Atlanta)

Please read our LLM Review Consent policy before submitting.
This research paper track and the competition track are two separate tracks with different submission requirements and evaluation criteria.

Schedule

All times are in Atlanta Time (GMT-4).

Atlanta Time (GMT-4)	Event
8:55-9:00	Opening Remarks
9:00-9:40	Invited Talk I
9:45-10:25	Invited Talk II
10:25-10:55	Poster/Break
11:00-11:40	Invited Talk III
11:40-12:10	Contributed Talks
12:10-13:30	Lunch
13:30-14:10	Invited Talk IV
14:15-14:55	Invited Talk V
15:00-15:30	Poster/Break
15:35-16:15	Invited Talk VI
16:20-17:00	Invited Talk VII
17:00-17:30	Contributed Talks
17:30-17:35	Closing Remarks

Challenge (Competition Track)

Lean Refactor Arena

Can agents make Lean proofs better, not just correct?

The Lean Refactor Arena is a two-track competition in verified proof refactoring. Participants build systems that rewrite existing Lean 4 proofs — drawn from active formalization projects and competition mathematics — while preserving their theorem statements and correctness.

Choose a track

Both tracks solve the same benchmark under different resource constraints.

Track 1

Closed-source LLM

Build a harness around closed-source frontier LLM APIs.

Budget: ≤ US$3 API spend per problem.

Track 2

Open-source LLM

Post-train open-source models, build a harness around them, or both.

Budget: must run on 4× 80 GB A100 · ≤ 48 h for the full benchmark.

How entries are scored

Every valid proof is evaluated on three complementary dimensions.

Proof size

Reduce proof-source token count compared with the reference proof.

Elaboration efficiency

Reduce the computational effort Lean uses to elaborate the proof.

Zero-shot version transfer

Keep the same proof compiling across other Lean toolchains.

Competition timeline

Phase	Dates	What happens
Warm-up	Now – Sep 30, 2026	The public development subset and the leaderboard are live. Submissions are accepted on the practice benchmark.
Full benchmark	October 1, 2026	The full benchmark is released and the leaderboard is refreshed. Entries are evaluated on the full benchmark from here on.
Deadline	November 8, 2026	Proof and code submissions close on the Arena site. Tech reports are due on OpenReview: https://openreview.net/group?id=NeurIPS.cc/2026/Workshop/VERICODEGEN_Competition
Review & awards	November 22, 2026	The organizers reproduce the top entries, and the winners of both tracks are announced.
Workshop	December 12, 2026	Each track winner gives a dedicated talk at the workshop in Atlanta.

Prize amounts and benchmark size are provisional and may be adjusted before September 1, 2026.

Submission and participation

Prepare your entry, or help us expand the benchmark.

Competition report

Every entry needs a tech report

Tech reports use the competition template (not the one for the research paper track): neurips_2026_vericode_workshop_competition.tex with neurips_2026_vericode_competition.sty, both in the same Overleaf project linked below. At least 4 pages, up to 9 pages, and submitted on OpenReview: https://openreview.net/group?id=NeurIPS.cc/2026/Workshop/VERICODEGEN_Competition

Tech reports are single-blind, so please do not anonymize them. We will invite Lean repository maintainers to review your submission and verify that it reproduces, which may involve contacting you directly. Include your real names, affiliations, and contact information so organizers can reach you about your code and submission during review.

Desk rejection: a missing required section (Approach, Models, Budget, Reproduction), exceeding your track’s budget, under-reporting what the run cost, not disclosing every model, or a run the organizers cannot repeat.

Open the report template on Overleaf Full rules: Tracks & Rules

Grow the benchmark

How to contribute

The benchmark grows with the community. We are looking for more Lean proofs to refactor, and we would love your input. A good candidate problem is long (so there is room to shorten), expensive to compile (it burns heartbeats, so there is real search in the proof), and stable across toolchains (the declaration appears verbatim at several Lean snapshots).

Maintain or know a Lean development with proofs like that? Read the contribution guide