Awesome Vericoding Awesome

License: CC0-1.0 PRs welcome Last commit sorry: 0 vibes: informally verified Q.E.D.

Vericoding logo: code braces around a check mark

Proof or it didn’t ship.

Vibecoding asks a model for code and hopes the tests catch the bugs. Sometimes it works, sometimes it doesn’t.

Vericoding asks for code and a proof that it meets a specification, then hands both to a verifier that doesn’t care who wrote them or how confident they sound. If the proof checks, the code does what the specification says, which leaves you two things to worry about: whether the specification says what you meant and whether the verifier can be trusted.

Bursuc et al. (2025) coined the term for LLM-generated, formally verified code, but people were doing the same thing by hand long before the models showed up. This awesome repo covers both: AI vericoding, and its artisanal ancestor, classic vericoding, where people still write the proofs themselves.

  Classic vericoding AI vericoding
Who writes the spec People People, often starting from AI drafts
Who writes code and proofs People, helped by SMT solvers and tactics Models and agents, guided by verifier feedback
Who checks the proofs A verifier or proof assistant The same verifier or proof assistant
Main bottleneck Expert time Specification quality and model capability

Naming convention: “Classic” vericoding is a retronym for what the field calls verified programming, auto-active verification, or proof-oriented programming. “AI vericoding” says AI rather than LLM on purpose: the lineage runs from pre-LLM neural provers such as Code2Inv and Proverbot9001 to today’s RL-trained provers and verifier-in-the-loop agents. Some authors split it further into inductive vericoding (sample, check, retry) and deductive vericoding (refine the spec into smaller specs, solve those, and compose the results).

flowchart LR
    intent([Intent]) -->|formalize and review| spec[Formal spec]
    spec --> author{Who writes code and proof?}
    author -->|people| classic[Classic vericoding]
    author -->|models and agents| ai[AI vericoding]
    classic --> verifier[[Verifier]]
    ai --> verifier
    verifier -->|errors and counterexamples| author
    verifier -->|proof accepted| done([Code with a machine-checked proof])

Legend: ⭐ good place to start · 🏭 used in production · 💰 paid

Contents

🚀 Start Here

Start here with zero assumptions

  1. Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken - A now-classic blog post from Google’s former Chief Java Architect about a bug that fooled everyone.
  2. When AI Writes the World’s Software, Who Verifies It? - Leonardo de Moura, creator of Lean, on why machine-checked proofs not more code review are the answer to AI-written software.

To write your first verified code by hand:

  1. Dafny Tutorial - Write and verify small programs with preconditions, postconditions, and loop invariants.
  2. Natural Number Game - Learn interactive proof in Lean by playing levels in the browser, no installation needed.
  3. Let’s Prove Leftpad - One small function proved in two dozen tools, so you can compare styles before choosing one.

To try AI vericoding:

  1. Prediction: AI Will Make Formal Verification Go Mainstream - A short, accessible case for why AI makes formal verification practical.
  2. Ask your coding assistant for a small Dafny method with its preconditions and postconditions, run dafny verify, and check the result against the Trust Checklist before believing it.

📐 Classic Vericoding

People write the proofs and machines check every step

📜 Foundations

Every verifier on this page runs on these ideas

📝 Essays

50+ years of arguing about whether proving programs is worth the trouble

🧩 Verification-Aware Languages

The verifier complains the moment your code and spec disagree

🔧 Verifiers for Mainstream Languages

Keep the language you ship and add the proofs

🧮 Proof Assistants

You and the prover close one goal at a time

🧱 Verification Infrastructure

The solvers and checkers that run every time you hit save

🏰 Verified Systems

Existence proofs for verified software at scale

📰 Industry Reports

What happened when big companies put proofs into production

📚 Books

For when the tutorial ends and the proofs get long

🎓 Courses and Tutorials

Homework graded by a verifier that never gives partial credit

📘 Official Cheat Sheets

Language tours already published on Learn X in Y Minutes

✏️ Unofficial Cheat Sheets

One page of syntax before your first proof obligation

🤖 AI Vericoding

The model writes the proof and you still own the spec

💬 Position Papers and Essays

The case for putting a verifier between AI and production

📖 Surveys

The map before the territory

📊 Benchmarks

Check what counts as solved before you quote a number

Benchmark Year Verifiers Size Task
CoqGym 2019 Rocq 71K proofs from 123 projects Proof synthesis
DafnyBench 2024 Dafny 750+ programs Annotation (hint) generation
FStarDataSet 2024 F* 32K definitions Proof-oriented program synthesis
MBPP-DFY 2024 Dafny 153 verified solutions Natural language to verified method
miniCodeProps 2024 Lean 201 specifications Proving program properties
Verus-Bench 2024 Verus 150 tasks Proof generation
CLEVER 2025 Lean 161 problems Specification, code, and proof
FVAPPS 2025 Lean 4,715 problems Code and proof from a specification
Vericoding 2025 Dafny, Verus, Lean 12,504 specifications Code and proof from a specification
VERINA 2025 Lean 189 tasks Code, specification, and proof
VerifyThisBench 2025 Several VerifyThis challenges Specification, code, and proof from natural language
VeruSAGE-Bench 2025 Verus 849 tasks from eight systems Systems proof tasks
AlgoVeri 2026 Dafny, Verus, Lean 77 algorithms Aligned cross-language vericoding
LCB-Pro-Dafny 2026 Dafny 250 problems Competitive programming
NTP4VC 2026 Isabelle, Lean, Rocq Linux and Contiki proof goals Proving verification conditions
VeriContest 2026 Verus 946 problems Code, specification, and proof
Verus-SpecBench 2026 Verus 581 tasks Specification autoformalization
Vero 2026 Lean 43 repositories Repository-level code and proof

✨ Verified Code Generation

Ask for code and get a receipt from the verifier

🧠 Proof and Annotation Synthesis

The code is written and the model has to convince the verifier

📋 Specification Generation

Read every spec a model writes before you trust the proof

🔄 Verified Translation

Rewrite it in Rust and then show nothing changed

🧪 Field Reports

AI provers meet real code and report what broke

🏆 Theorem-Proving Models

Olympiad math tricks that carry over to program proofs

🔌 Agent Tooling

Plumbing that shows an agent the exact proof state

🏢 Organizations

Follow the money and the provers

🔍 Trust Checklist

Search for these escape hatches before you trust a ✅

Verifier Escape hatches to search for How to audit
Dafny assume, {:axiom}, {:verify false}, bodiless {:extern} declarations dafny verify --warn-contradictory-assumptions --warn-redundant-assumptions
Verus assume(...), #[verifier::external_body] Search for both and review every trusted function specification
Lean 4 sorry, axiom, native_decide, @[implemented_by], @[extern] #print axioms theorem_name lists every axiom a theorem depends on
Rocq Admitted, admit, Axiom, Parameter Print Assumptions theorem_name
Isabelle sorry, axiomatization thm_oracles theorem_name shows skipped proofs
F* admit (), assume, --admit_smt_queries true, --lax Search sources and build flags
SPARK pragma Assume, SPARK_Mode (Off), pragma Annotate justifications Review the GNATprove summary for assumed and justified checks
Kani kani::assume, function stubs, low unwinding bounds Remember that the proof only covers the bounds you set

📅 Milestones

From Floyd’s flowcharts to agent-written proofs in under sixty years

Year Milestone Why it matters
1967 Floyd’s inductive assertions Program correctness becomes a matter of proof.
1969 Hoare logic Pre/postcondition triples become the core of program verification.
1975 Dijkstra’s weakest preconditions Programs and proofs can be derived together.
1986 Eiffel and Design by Contract Specifications become part of everyday code.
2002 Separation logic Local reasoning about pointer-manipulating programs.
2008 Z3 Fast SMT solving makes auto-active verifiers practical.
2009 seL4 and CompCert Full functional correctness for an OS kernel and an optimizing compiler.
2010 Dafny Verification-aware programming with feedback as you type.
2017 HACL* ships in Firefox Verified code reaches a mainstream product.
2018 Code2Inv Neural networks start proposing loop invariants.
2019 CoqGym A large learning environment for machine-written proofs.
2020 GPT-f Transformers start writing formal proofs.
2023 Verus Verified Rust for low-level systems code.
2023 Baldur and Clover LLMs write whole proofs and verified programs.
2024 DafnyBench and AlphaProof Benchmarks for AI vericoding; RL provers reach olympiad level.
2025 The vericoding benchmark The field gets a name and a 12,504-specification benchmark.
2026 Agents on real systems Agent-written proofs land upstream and benchmarks move to whole repositories.

🌍 Community

Where verification people compete and argue

🥇 Competitions

Verifiers race on scoreboards and people race the clock

🎤 Venues

Where the papers on this list get argued over in person

💭 Forums

Where to ask why your proof won’t go through

📣 Blogs

Shorter than papers and more candid about what went wrong

🔗 Meta

Neighboring lists for when this one runs out

Contributing

Contributions are welcome. Read the contribution guidelines first, and suggest resources through the issue form if you prefer not to open a pull request.