Nine Rules for Vibe Validation of Vibe-Coded Algorithms

Using AI-Written Lean to Validate AI-Written Rust

Last year, I used AI-written Lean to prove the mathematical correctness of an algorithm I had written in Rust. It was part of an open-source library that now has more than 5 million downloads. I knew almost no Lean and did almost none of the proof work myself. I called the approach Vibe Validation. After about three weeks of part-time work and hundreds of back-and-forth prompts, I had a machine-checked proof of an algorithm I cared about.

It’s now a year later. Frontier AI models are solving mathematics problems with million-dollar prizes attached to them. Surely validating algorithms is easier now. So I returned to vibe validation to see what had changed. Are these new AIs genies that are now ready to grant all our validation wishes?

Scope: I’m validating a high-level algorithm, not every detail of its Rust implementation. I translate the algorithm into Lean, have AI write a proof that the Lean version does what I expect, and have Lean check the proof. I separately test and review whether the Rust and Lean versions match. This works best for algorithms whose intended behavior can be stated precisely. Rust and Lean are the languages I happen to use; the approach is not tied to either.

In this return to vibe validation, I found three things:

• Proofs that once took weeks can now be done in tens of minutes with just one or two prompts. I never tested the same proof with both last year’s and this year’s AI models, so this is not a controlled comparison. Still, the difference in effort was striking.
• In some domains, the AI can now create an algorithm and then validate it in Lean. It did this several times, including two of the project’s most complicated new algorithms. It wrote the Rust, translated the algorithm into Lean, and then constructed a proof that Lean checked. In those cases, the AI directly addressed a central problem of AI-generated code: how do we know the generated algorithm is correct?
• AI-written proofs accumulate slop, but AI can refactor much of it away. I had the AI measure the Lean proof using several metrics, not just lines of code, then simplify and reorganize it. Lean checked every change, making aggressive vibe refactoring formally safe. The cleaner Lean code also seemed to make later proofs easier.

Aside: Is AI for coding good or bad for society? To use an oxymoron, I feel strongly ambivalent. I do think one thing is clearly good: too little code gets validated because validation has been too hard. AI changes that.

We’ll follow the story mostly in the order it happened. A prelude cleans up last year’s proof and yields Rules 1–4. Then we follow one new cursor algorithm through four stages: Code, Specify, Review, Validate, which yield Rules 5–9. A coda follows the same workflow into harder problems. We’ll conclude with lessons, a comparison to last year’s nine rules, and three unfulfilled wishes.

The nine rules are:

1. Don’t prompt. Meta-prompt.
2. Reduce slop with aggressive but safe three-step vibe refactoring: Local, Shared, Higher-Level.
3. Enforce correctness guardrails.
4. Measure slop with a dashboard of metrics, rather than lines of code alone.
5. Vibe Code. Vibe Specify. Vibe & Human Review. Vibe Validate.
6. Preserve the algorithm; abstract the details.
7. Review adversarially with both human and AI eyes.
8. Set up the theorem first; prove it second.
9. Prove related results in sequence and build a shared library as you go.

Prelude: Clean up last year’s proof (Rules 1–4)

The code in this story comes from RangeSetBlaze, a Rust library with 5 million downloads. It represents sets and maps of integers compactly, using ranges. A set is stored as sorted, non-overlapping, non-adjacent ranges. For example:

[101..=102, 400..=402, 404..=405]

If we insert 402..=404, RangeSetBlaze merges the touching ranges and produces:

[101..=102, 400..=405]

Last year, via vibe validation, I proved one of RangeSetBlaze’s two central insertion algorithms correct. Lean accepted the proof, meaning the theorem followed from its assumptions. Just as important, I could read the theorem statement and its assumptions and see that they expressed the correctness property I wanted to prove.

Aside: Compared to your programs, I likely picked an easy target for formal validation. Range sets and range maps have clear mathematical meanings, so we can state what an algorithm should do without depending on the details of its Rust implementation. That makes RangeSetBlaze easier to validate than many ordinary application programs. But it is not unique. The same methods should apply wherever the intended behavior can be stated precisely.

Last year’s proof effort required hundreds of prompts and produced a 4,791-line Lean project devoted mainly to validating one production insertion algorithm. The corresponding Rust path occupied just 67 code-bearing lines. Some of that difference was the unavoidable cost of formal proof, but some was accumulated proof slop: duplicated lemmas, unnecessary helper theorems, overly explicit arguments, and abstractions that once helped but no longer earned their keep.

So before asking the AI to prove anything new, I asked it to clean up the old proof.

I mostly used one long-running, quota-free ChatGPT Sol 5.6 chat to develop prompts for fresh Codex Sol 5.6 sessions in VS Code. I also asked Codex Sol to delegate suitable work to cheaper Codex Luna subagents. Later, after exhausting my Codex quota, I also used Claude Code with Sonnet 5 and some Fable 5.1 credits. I found Sol 5.6 and Fable 5.1 very strong, Sonnet 5 good, and Luna mixed but cheap.

Rule 1: Don’t prompt. Meta-prompt. Have one long-running chat write prompts for fresh coding sessions. The long-running chat keeps the context; the coding agents get clean, focused instructions.

Lean’s proof checker let me refactor aggressively. I could ask the AI to delete helpers, combine lemmas, reorganize files, replace home-grown machinery with standard Lean results, and let Lean infer more. After every change, Lean still had to accept the same correctness theorem, with no sorry placeholders in the finished proof, no new axioms, or other shortcuts.

The cleanup worked. The main proof file fell from 3,320 total lines to 942, a 72 percent reduction. More important, lines containing Lean code fell from 1,983 to 777, a 61 percent reduction. This was not just code moving elsewhere: all other Lean files combined gained only 11 code-bearing lines.

Rule 2: Reduce slop with aggressive but safe three-step vibe refactoring: Local, Shared, Higher-Level.

The steps:

1. Local: Simplify one file or proof, using Lean’s Mathlib (its standard library) where possible.
2. Shared: Find common structure across files and proofs, then extract reusable lemmas.
3. Higher-Level: Replace detailed proof steps with larger steps that Lean can infer.

I used to joke with my manager that I could make our program as fast as he wanted, as long as it didn’t have to be correct. The same applies to proof cleanup: we can make a proof wonderfully short if we let it become wrong or vacuous. With that in mind:

Rule 3: Enforce correctness guardrails. Require the project to build and the main proof file to compile directly; allow no sorry in the finished proof and no new axioms. In Lean, sorry means roughly, “there should be a proof here, but accept this statement for now”.

Given those guardrails, can we just ask the AI to play “code golf” and minimize lines of code? No. Line count does not capture proof complexity. So should we just invent a single, perfect complexity metric? Again, no.

Rule 4: Measure slop with a dashboard of metrics, rather than lines of code alone.

Track several measures of proof complexity. Start with the list below, which the AI suggested when I asked how to measure proof slop. You don’t need to understand every Lean term; give the list to your coding agent, ask it to measure your proof and suggest additions or changes, then make refactorings that, on balance, improve the dashboard.

The metrics I used:

• Size: total lines and lines containing Lean code.
• Proof branching: counts of cases, by_cases, and induction.
• Proof plumbing: counts of intermediate facts and manual goal manipulation, such as have, show, suffices, and rw.
• Automation: counts of tactics such as simp, simpa, omega, linarith, and grind.
• Representation machinery: uses of list-specific operations such as List.span, takeWhile, dropWhile, getLast?, and dropLast.
• Proof API shape: counts of public and private lemmas and theorems.

The dashboard snapshot below focuses on the main proof file. The final Size row checks the whole Lean project, guarding against making the main file smaller merely by moving code elsewhere.

Metric                                      Before   After   Change
------------------------------------------------------------------
Size
 Total lines 3,320 942 -72%
 Lines containing Lean code 1,983 777 -61%
 Whole project: lines containing Lean code 3,252 2,057 -37%
Proof API
 Public lemmas/theorems 6 6 0%
 Private lemmas/theorems 36 17 -53%
Proof branching
 cases 56 6 -89%
 by_cases 17 5 -71%
 induction 23 3 -87%
Proof plumbing
 have 471 133 -72%
 show 8 3 -63%
 suffices 1 0 -100%
 rw 172 41 -76%
Automation
 simp 203 50 -75%
 simpa 18 27 +50%
 omega 15 5 -67%
 linarith 3 0 -100%
 grind 0 0 0%
Representation machinery
 List.span 44 22 -50%
 takeWhile 81 24 -70%
 dropWhile 66 7 -89%
 getLast? 7 8 +14%
 dropLast 10 2 -80%

Notice that not every number went down. simpa and getLast? increased. That is fine. The goal was not to minimize every metric, but to simplify the proof on balance.

Aside: I don’t know for sure that simplifying the proof makes later validation easier, but I strongly, strongly suspect it does. One could run a real experiment. I didn’t.

With the old proof cleaned up, I turned to creating a new algorithm.

First, Vibe Code (Rule 5)

I wanted a faster range-insertion algorithm for RangeSetBlaze. Internally, RangeSetBlaze stores its ranges in Rust’s BTreeMap, a standard collection that keeps key-value pairs sorted by key. An experimental BTreeMap cursor API offered a potentially faster way to implement insertion.

I could have learned the cursor API and written the new algorithm myself. But I didn’t. Instead, following Rule 1, I meta-prompted for a detailed coding prompt: write a cursor-based insertion algorithm with the same behavior as the existing one, test the two against each other, and benchmark them.

Codex Sol produced and tested the cursor-based set algorithm in twelve minutes, from one substantive coding prompt plus a short continuation after a quota interruption. The implementation passed the existing automated tests.

Codex Sol also wrote and checked in new tests specifically for the new algorithm. Some tests ran the old and new algorithms side by side on identical inputs and compared their results. Others tried every possible starting set made from the integers 0 through 6, combined with every possible range to insert, for 6,272 comparisons in all. A third performed 20,000 successive randomized insertions.

Codex Sol also built a benchmark that compared the two algorithms in the same program. In the first timing run, repeated insertion ran 2.07× as fast as the old algorithm. I committed the work twenty minutes later, leaving the new algorithm optional because it depends on an experimental Rust feature.

How different was the new cursor algorithm from the old algorithm? I’d say “half different”. The high-level idea stayed the same: insert a range and absorb any stored ranges that touch or overlap it. For example, inserting 4..=8 into [1..=3, 7..=9] must produce [1..=9]. But nearly every implementation detail changed. Apart from basic setup and bookkeeping, the two versions share essentially no source lines, and even their functions are organized differently. The new version was actually a little longer: 72 code-bearing lines versus 57 for the old one.

So, we now have more than 70 lines of mostly new Rust code. Can we trust it? Is it correct? The old and new tests give us confidence, but they may still miss an edge case. Formal validation gives us certainty about the high-level algorithm: with respect to our specification, it is correct for every possible input.

That suggests a four-step workflow:

Rule 5: Vibe Code. Vibe Specify. Vibe & Human Review. Vibe Validate.

Second, Vibe Specify (Rule 6)

Now Codex had to turn the Rust algorithm into something Lean could reason about mathematically.

Aside: Rust is a multi-paradigm language. It supports both imperative, step-by-step code and functional styles. The cursor algorithm is mostly imperative: move through a tree, inspect neighboring ranges, remove some, and insert another. Lean is more naturally functional, so Codex represented those state changes by producing new lists rather than modifying a tree in place.

Last year, I translated the Rust algorithm into Lean by hand. This year, Codex did it. Following last year’s approach, Codex did not reproduce the Rust code line by line. Instead, it modeled the relevant BTreeMap behavior with Lean lists. In particular, it modeled a BTreeMap cursor as a position between two lists: ranges already passed on the left and ranges still to process on the right.

Rust cursor:
 [1..=3] | cursor | [7..=9] [20..=22]
Lean model:
 left = [1..=3]
 right = [7..=9, 20..=22]

Looking at the next range meant inspecting the first item on the right. Removing that range meant continuing with the rest of the right-hand list. Inserting before the cursor meant rebuilding the lists around the new range.

This preserved the decisions that mattered for correctness: which ranges to keep, extend, absorb, or insert. The details of navigating and modifying a Rust BTreeMap disappeared. The Lean version was not a line-by-line translation, but a simpler functional model of the same insertion algorithm. We’ll return to modeling BTreeMap semantics in the coda.

Rule 6: Preserve the algorithm; abstract the details. Have the coding agent model the decisions and state transitions of the real implementation in a form simple enough to prove, but still close enough to review against the original code.

As noted earlier, this validates the algorithm, not every detail of the Rust implementation. That abstraction is the point. I reviewed the Lean version of the algorithm against the Rust code, while Rust tests separately compared the old and new Rust implementations.

Next came the specification. In this case, the cursor algorithm did not need a new specification. It was supposed to do exactly what the old insertion algorithm did: produce the union of the original set and the inserted range, represented as sorted, non-overlapping, non-adjacent ranges. We’ll revisit creating new specifications when we discuss insertions for maps.

At this point, Codex had two things in Lean: a model of the new algorithm and a precise statement of what that algorithm must do. Before trying to connect them with a proof, I wanted to review both.

Third, Vibe & Human Review (Rule 7)

Before asking Codex to prove anything, I wanted another look at the three pieces we were about to trust: the Rust algorithm, the Lean version of the algorithm, and the Lean specification.

For the Rust code, the first question was simple: did Codex actually implement a new cursor-based insertion algorithm? It could have copied the old algorithm, wrapped it differently, or invented some unrelated approach that happened to pass the tests. I wanted to verify that the new code really used the cursor API to perform range insertion.

For the Lean version, the question was different: did Codex preserve every decision that matters for correctness?

For the specification: could the theorem be true while the algorithm still did something I would consider wrong?

Some of this review should be human. I wanted to understand the important parts myself, especially the top-level algorithm and the statement being proved. But AI gives us another useful tool: use a fresh session, preferably with a different strong AI model, and ask it to be adversarial rather than helpful.

Don’t ask, “Does this look correct?” Ask it to find a counterexample, a missing assumption, a mismatch between Rust and Lean, or a specification that is too weak.

Rule 7: Review adversarially with both human and AI eyes.

Here is the small piece of Lean I most wanted to understand myself. It states that the insertion algorithm produces exactly the mathematical union of its inputs:

theorem internalAddD_toSet (s : RangeSetBlaze) (r : IntRange) :
 (internalAddD s r).toSet = s.toSet ∪ r.toSet := by

Even with very little understanding of Lean, I can read the important claim: after inserting r, the represented set must equal the original set union r. Separately, I needed to verify that RangeSetBlaze enforces the representation invariant I care about: sorted, non-overlapping, non-adjacent ranges.

That is the level of understanding I want before trusting the proof. I do not need to understand every line of Lean that follows, but I do want to know that the algorithm being modeled is the one I intended, and that the theorem being proved says what I mean by “correct.”

Fourth, Vibe Validate (Rules 8 and 9)

Now Codex had a reviewed Lean version of the algorithm and a reviewed specification. The remaining job was to connect them: prove that the algorithm satisfied the specification for every valid input.

Following Rule 1, I had my long-running chat create two focused prompts for fresh coding sessions. The first asked Codex Sol to set up the theorem and proof structure, temporarily using sorry where necessary. The second asked Codex Sol to replace every sorry with a real proof.

Rule 8: Set up the theorem first; prove it second.

Last year, getting from an algorithm and specification to a completed proof took weeks of part-time work and hundreds of prompts. This year, for the cursor algorithm, the same stage took tens of minutes and just two prompts.

Perhaps this proof simply happened to be much easier. That is possible. But its size and the other proof-complexity metrics were roughly comparable to those of last year’s proof. And, as we’ll see, later I gave the same workflow substantially harder proofs with similar results.

Rule 8 was about proving one theorem. Rule 9 is about building up a collection of related proofs.

Software development often works incrementally: get something working, then build on it. Formal proof can work the same way. Prove one useful result, then let its definitions, lemmas, and abstractions become infrastructure for the next proof.

But incremental work can accumulate slop: duplicate lemmas, obsolete adapters, overly specific helpers, and temporary abstractions that outlive the proof step that motivated them. So periodically return to Rule 2 and clean up what has accumulated.

Rule 9: Prove related results in sequence and build a shared library as you go.

The result is a proof library that makes the next validation easier. Indeed, if you are validating algorithms involving range sets or ordered maps, my Lean library may be directly useful to you.

Coda: And Then I Just Kept Going

The cursor insertion proof was not the end. Once the proof library and workflow were working, I kept asking, in effect, “Okay, you proved that. What about this?” I felt as if I had a magic genie that would grant not just three wishes but as many as my subscription quotas allowed.

The timeline below shows what I asked for next and roughly how long each step took. The times are mechanically calculated elapsed wall-clock time between commits, not working time, so they include sleeping, meals, errands, and everything else. Unless noted otherwise, each step followed the same cycle: Code, Specify, Review, Validate, Clean Up.

Timeline

• Existing Set Insert Algorithm — 1.784 days: Set up and cleaned up last year’s proof. As described above.
• Cursor Set Insert — 0.902 days: As described above.
• Simplified Map Insert — 0.123 days: Up to this point, I had validated only set algorithms. Now I moved to maps. RangeMapBlaze stores values along with ranges, so insertion adds a (range, value) pair rather than just a range. Based on the Rust code, I consider map insertion roughly two or three times more complex than set insertion. As I had done last year, I first asked the AI to create a simpler, Lean-only reference algorithm. It was deliberately inefficient, but easy to reason about. It let me check the map-insert specification while the AI built up proof machinery in Lean.
• Production Map Insert — 0.088 days: The Rust algorithm already existed, and I had wanted to validate it since last year. With the new tools and the simpler map proof as a foundation, I did it in just over two hours.
• Cursor Map Insert — 0.540 days: Could the AI write a production Rust map-insert algorithm using BTreeMap cursors? Could it prove the algorithm correct? Yes to both.
• Prove Length Updates — 0.444 days: The real Rust insertion code does more than update the BTreeMap. It also maintains a cached length: the number of individual integers represented. I had never proved that bookkeeping correct. This time I did, for all four insertion algorithms: production and cursor versions, for both sets and maps.

Aside: Some of the length proofs used signed integers, while others used Lean’s natural numbers (Nat). With Nat, subtraction truncates at zero, so proving the desired equality required showing that each subtraction really was nonnegative. That gave me an extra guarantee about the corresponding Rust code, which uses unsigned integers and must not underflow. So I switched all the length proofs to Nat.

• Prove Canonical Uniqueness — 0.516 days: I’ve always intended RangeSetBlaze and RangeMapBlaze to have canonical representations. In other words, every mathematical set, and every mapping from integers to values should have exactly one valid internal representation. I had always assumed this property but had never proved it. Now I asked the AI to prove it in Lean. It did.

Aside: By this point, I had started bundling the whole workflow into one prompt when I could: Rust implementation, Lean model and specification, proof, tests, and cleanup. If something went wrong, I broke the job into smaller prompts. For the next proofs, the AI implemented the cursor versions and validated both the baseline and cursor algorithms in Lean.

• range_or_gap_at — 0.044 days: Insertion is not the only operation that matters. RangeSetBlaze and RangeMapBlaze should also tell you which stored range contains a given integer or, if none does, the surrounding gap, including gaps at the ends. I already had non-cursor Rust methods for sets and maps. I had the AI invent cursor-based versions in Rust, then specify correctness in Lean: the answer must be the maximal range or gap containing the queried integer. The AI proved in Lean that both the baseline and cursor algorithms satisfy that specification.
• Formal but Partial BTreeMap Semantics — 0.235 days: The Lean proofs model the BTreeMap operations the algorithms need using a list kept in sorted order, rather than modeling BTreeMap itself. I had the AI express those semantics as a small Rust trait, roughly an interface in other languages. It then implemented the trait twice: once with a sorted Vec and once directly with Rust’s BTreeMap. Ordinary comparison tests, not formal proofs, checked that the two implementations had the same observable behavior. You can read the Rust semantics and implementations.
• Compare five AI agents on the same proof — 0.229 days: I did run one controlled experiment. I tested five agents: DeepSeek V4.1 Flash, Sonnet 5, Luna 5.6, Fable 5.1, and Sol 5.6. The task was to prove that range-set insertion could be implemented in terms of range-map insertion. I already knew the key idea: set insertion can be treated as a special case of map insertion when every value is the same (Unit in Rust and Lean). I believe this to be a relatively easy proof. I gave the same task independently to all five agents. DeepSeek Flash failed to complete it. I then blinded the four successful results and had Fable and Sol judge them independently. They and I agreed on the same order: Fable > Sol > Sonnet > Luna. In the end, I had Sol combine the best parts of the Fable and Sol solutions and added the result to my Lean proof repository.

So, in five days, working part time, I was done. Updated benchmarks showed geometric-mean speedups of about 2.0× for sets and 1.7× for maps.

After a bit more review and updated documentation, I released a new version of RangeSetBlaze. It includes the optional cursor algorithms, new “Range or Gap” functions, and, unrelated to what we’ve discussed here, stable support for floating-point intervals.

Conclusion

I came back to vibe validation with two goals: clean up last year’s proof and prove the original map-insertion algorithm correct. I got both, and more. The AI also wrote and validated new algorithms, including cursor-based versions that ran substantially faster than the originals. The AI also helped extend the proof library to several other important properties and operations.

Just as important, new proofs in the same domain now come much more readily. That seems to result from both a cleaner RangeSetBlaze Lean proof library and today’s more capable LLMs.

Validation makes a proof trustworthy; refactoring makes it reusable.

Looking back at last year’s nine rules, most still hold. I still think you can use Lean without really learning it, that you should define the mathematical concepts carefully, and that you should audit both the Rust-to-Lean translation and the final proof. I now feel even more strongly about using one AI to guide another and about reshaping concepts into forms Lean handles naturally. What has weakened is the need to proceed cautiously through toy and simplified algorithms before attempting the real one. Today’s stronger models can often go straight to the harder proof.

In the coda above, I compared this year’s AI to a magic genie whose wishes are limited by my subscription quotas. I still, however, have three not-yet-fulfilled wishes:

• Show that vibe validation works for algorithms whose intended behavior is harder to specify precisely.
• Close more of the gap between Rust and Lean, by automating the translation and taking at least one important algorithm down to detailed Rust semantics.
• Validate every important RangeSetBlaze algorithm at this high level.

Happily, people, and I imagine some AIs, are already working on these problems. The Rust Formal Methods Interest Group provides a good map of the territory, including Aeneas, Creusot, Kani, MIRAI, Verus, RefinedRust, and other approaches to Rust verification. Much of this work operates closer to the Rust implementation than the high-level algorithm validation I’ve explored here. Some of it also addresses my remaining wishes directly, including translating Rust into forms suitable for theorem provers.

As these wishes are granted, vibe validation could stop being something we do only for a few especially interesting algorithms. It could become something we can reasonably ask of every algorithm that lends itself to specification.

Thanks for following along with this return to vibe validation. The Lean code is on GitHub. I hope some of these rules prove useful when you ask AI not only to write an algorithm, but also to help validate it.

Aside: If you’re interested in future articles, please follow me on Medium. I write on scientific programming in Rust and Python, machine learning, and statistics. I tend to write about one article per month.

Aside: If you’re interested in future articles, please follow me on Medium. I write on scientific programming in Rust and Python, machine learning, and statistics. I tend to write about one article per month.

Nine Rules for Vibe Validation of Vibe-Coded Algorithms was originally published in Level Up Coding on Medium, where people are continuing the conversation by highlighting and responding to this story.