Proveit.
Formal verification, Lean, and how AI is learning to check its own work .
Featuring: an exploding rocket, a buggy chip and a very confident chatbot.
[Let the rocket fly and the title land. No need to talk over it.]
Hi, I'm Abhiraj.
A small disclaimer before we start. I'm not a mathematician. I build software for a living. A while ago I fell down a rabbit hole about how we actually know software works, and this talk is mostly me sharing what I found down there. Including the parts I'm still confused about.
[Make the rabbit-hole line true to you: when and why you got into this.]
It does involve a bit of maths. But there's exactly one equation in the whole talk, and you can hold me to that.
The question I kept coming back to is pretty simple. How do we know a program does what it's supposed to do?
And the honest answer, most of the time, is that we don't, really. We test it, we feel reasonably good about it, and we ship it.
There's another way, called formal verification, where you prove a program is correct, with maths. It's been around for decades and mostly ignored, because it was painfully expensive. What got me interested is that AI seems to be changing that. Which is a strange sentence, given how much AI makes things up. So that's the puzzle for today.
But I want to start with a rocket.
[click]
01 · June 4, 1996 · Kourou
Ariane 5.
Mission clock T−3.0
horizontal_bias float64 → int16 · reused from Ariane 4
0 max int16 = 32,767
Operand error → guidance computer down → its error code read as flight data
$370M
Tested for years. Never on Ariane 5's trajectory.
June 4th, 1996. Kourou, French Guiana. That's where Europe launches its rockets.
This is Ariane 5. Europe spent about ten years and roughly seven billion dollars building it. It's the big new successor to Ariane 4, which had been very reliable. This is its first flight. On top are four science satellites called Cluster, meant to study how the solar wind hits Earth's magnetic field. Nobody on board.
Let's launch it. You're welcome to count down with me. I won't make you.
[Press →. Count down quietly: three, two, one.]
So far, so good.
While it climbs, keep an eye on the little box on the left. That's one number inside the navigation computer. Roughly, it tracks how fast the rocket is drifting sideways.
The software stores this as a big decimal number. Then at one point it copies it into a much smaller box, a 16-bit integer, which can only hold numbers up to 32,767.
This code was reused from Ariane 4. On Ariane 4, that number never got close to 32,767. So years earlier, someone quite reasonably decided this conversion didn't need a safety check.
Ariane 5 is a lot faster. So the number gets bigger… and bigger…
[Boom. Let it sit for a second.]
…and it doesn't fit.
Thirty-seven seconds in, the navigation computer overflows and shuts down. There was a backup computer, of course. It was running the same code, with the same numbers, so it had already failed the same way, a fraction of a second earlier.
Then the main flight computer received the error message and read it as flight data. As far as it could tell, the rocket had suddenly swung way off course. So it corrected, hard. The rocket turned sideways at full speed, the air tore it apart, and the self-destruct finished it off.
The detail I can't get over: the calculation that crashed wasn't even needed after liftoff. It was left over from Ariane 4 and kept running for about forty seconds after launch, just in case. It had nothing to do. And it brought the whole thing down.
[click]
And the code had been tested. For years. It had flown on Ariane 4 many times without a problem. It was just never tested with Ariane 5's flight path.
About 370 million dollars, in 37 seconds, because one number didn't fit in its box.
What I find unsettling is that nobody here was careless. These were very good engineers making reasonable decisions. Which made me wonder how often this kind of thing happens. Turns out, two years earlier, it happened to Intel.
⚠ $370M is the commonly cited figure (rocket plus payload); sources vary. The backup unit failed 72 ms before the primary; the alignment function kept running about 40 s after liftoff. The Cluster satellites were rebuilt and launched in 2000.
02 · October 1994
Pentium
A maths professor's new chip got division wrong.
5 missing table entries
Intel: once per 27,000 years
IBM: every 24 days
$475M write-off
The famous division
Correct
Pentium
1994. Lynchburg College, Virginia. A maths professor called Thomas Nicely is working on a number theory problem that involves adding up the reciprocals of twin primes. You don't need to know what that means. I had to look it up too. What matters is that it needs a lot of very precise division, and he's running it on a few computers, including a new Intel Pentium.
Around June, his results stop matching. So he assumes he's made a mistake, which, to be fair, is what I'd assume too. He checks his code. Then his maths. Then the compiler. This goes on for months. By October he's fairly sure it isn't him. It's the chip.
[Let the division type out]
This is the well-known example. 4,195,835 divided by 3,145,727. The correct answer starts 1.33382. The Pentium said 1.33373. It goes wrong at the fourth decimal place.
He emails some colleagues, they forward it on, and within a few weeks it's all over the early internet. Then it's on CNN.
[click]
The cause turned out to be a lookup table on the chip that helped it divide quickly. It had 1,066 entries. Five were missing.
Intel had actually found the bug themselves months earlier and decided not to mention it. Once it was public, their position was roughly that an average user would hit it once every 27,000 years. Which is the corporate version of "works on my machine."
IBM did its own estimate, got something closer to once every 24 days for a heavy spreadsheet user, and stopped shipping Pentium machines.
The internet, of course, made jokes. My favourite one: how many Pentium designers does it take to screw in a light bulb? 1.99904274017. But that's close enough for non-technical people.
[Small pause. If it doesn't land, that's fine. It's a 1994 joke.]
Intel eventually offered a replacement to anyone who asked, and took a 475 million dollar charge.
So, a rocket and a chip. Careful people, lots of testing, both wrong. That was the part that bugged me. If testing didn't catch these, what exactly was it missing?
[click]
Both were tested · so what's wrong with testing?
Let's vibe-code something.
Six tests passed.It still prints money.
Ship it?
So what's wrong with testing? I wanted to see it go wrong on something small. And these days, the most relatable way to write something small is to ask an AI to write it for you.
[The prompt types itself]
So let's vibe-code something. A withdraw function for a wallet app. Keep it simple.
[The code appears]
And it does. Honestly, this looks fine to me. If the amount is less than your balance, take it out. Otherwise, refuse. I've seen worse code in production. I've written worse code in production.
[The tests run]
Let's test it. Withdraw 30 from 100: 70. Correct. Withdraw everything: zero. Withdraw more than you have: refused. Withdraw from an empty wallet: refused. Half a rupee, zero rupees. All pass.
Six tests, all green. If this were a pull request, I'd probably approve it.
[The "Ship it?" sticker appears]
Ship it?
[click]
Withdraw minus fifty.
Minus fifty is less than a hundred, so the check passes. And a hundred minus minus fifty… is a hundred and fifty.
[Pause.]
You withdrew money and your balance went up. This wallet prints money.
None of the six tests tried a negative number, because none of us thought of it. Which is exactly what happened with Ariane. The tests were fine. They just never tried the case that mattered.
So if all your tests pass, how would you actually know you're safe?
[click]
⚠ Negative-amount bugs are a well-known class of real payment bugs. Don't name a specific incident unless you've checked it.
So how would you know for sure?
Tests check a few points.
A proof checks every one.
The rule · my one equation (ish)
balance after ≤ balance before For every balance. For every amount.
if (amount <= 0) return balance;
↓ the 6 amounts we tested
−∞ −50 0 100 +∞
✗ stuck: −50 makes it go up
✓ Proved for every amount
The honest answer is: with tests alone, you wouldn't.
[Point at the line]
Think of every amount someone could possibly type in as this line. Negative numbers on the left, huge numbers on the right, every decimal in between. Infinitely many.
Our six tests are these yellow dots. All bunched up on the right, around the numbers we'd naturally think of. The whole left side, nobody looked at.
You could add a hundred more tests. A million. You'd still just have dots on a line that goes on forever.
[click]
A proof works differently. Instead of trying amounts, you write down the rule you actually care about. Here it's: after a withdrawal, your balance should never be higher than before. That's my one equation for this talk. Technically it's an inequality, which I'm told is worse.
Then you try to prove that rule for every balance and every amount at once. Not some of them. All of them.
[The line fills in]
For positive amounts, it works. But the proof gets stuck on the left side. It can't show the rule holds for negative amounts, because it doesn't. And the place where it gets stuck points straight at the bug. Nobody had to think of minus fifty.
[click]
So we fix it. One line: if the amount isn't positive, refuse.
And now the proof goes through. For every amount. Minus fifty, three trillion, numbers nobody will ever type.
This was the bit that made it click for me. Testing checks the cases you thought of. A proof also covers the ones you didn't. Ariane's engineers didn't think about Ariane 5's flight path. Whoever wrote these tests didn't think about minus fifty. A proof doesn't need you to.
[Pause.]
Paris, 1998
Metro Line 14.
Driverless. Proved with the B-Method before a single passenger boarded.
14
0
bugs found in the proved code since
[The metro is on screen. Tell the chip part first, then turn to the train.]
So did anyone actually do this? Yes, and the chip industry got there first.
After the Pentium mess, chipmakers did the maths on testing and didn't like the answer. A modern chip can be in more possible states than there are atoms in the universe. You can't test your way through that. So they started proving instead.
In 1996, AMD proved the division in its K5 chip correct, before it shipped. I like to think AMD had been watching Intel's year quite closely. Two years later, Intel hired a mathematician, John Harrison, to prove its floating-point maths. Today it's routine in chip design. Parts of the chip in your laptop were probably checked more rigorously than most of the software running on it.
And it isn't just chips.
October 1998. Paris opens Metro Line 14. The trains have no drivers.
Would you get on? [Let people answer. Someone usually says no.]
I think I'd hesitate. And the people building it seem to have expected that. So the safety software, the part that decides when trains move, stop and open their doors, was built with something called the B-Method, from a French computer scientist, Jean-Raymond Abrial.
As I understand it, with the B-Method you start by writing down exactly what must never happen. Things like: two trains are never on the same stretch of track. Then you prove, step by step, that the code can't break those rules.
About 86,000 lines of safety code. About 27,800 proofs. And no bugs found in the proved code since it opened.
It's been running for over twenty-five years. So if you've ridden Line 14, you've technically ridden inside a proof. Which is a slightly odd thing to know about a train.
Chips and trains could afford it.
Everyone else couldn't.
One proof, by hand
0 years
Rooms of PhDs. Years. Heroic amounts of coffee.
So I had the obvious question at this point. If proofs work this well, why isn't everything proved? Why are most of us still writing tests and hoping?
[click]
The answer, it turns out, is mostly cost.
The example that stuck with me is seL4, a small operating-system kernel. About ten thousand lines of code. Proving it correct took experts roughly twenty person-years. Twenty years of very skilled work, for ten thousand lines. Most of the apps I've worked on are a lot bigger than that.
So proofs meant a room of PhDs, a few years, and a lot of coffee. Intel can justify that, because one bug cost them half a billion dollars. A metro can justify it, because lives depend on it. A typical app, or a smart contract someone wrote over a few weekends, can't.
So for roughly twenty-five years, that's how things stayed. Rockets, chips and trains got proofs. Everything else got tests, and hope.
I'd mentally filed all this under "nice idea, too expensive." Then something from a completely different field made me look again.
⚠ seL4: about 10,000 lines of C; the commonly cited effort is around 20 person-years including tools.
Meanwhile, in another lab
AlphaFold · biology
Protein structures
0
PREDICTED BY AI
GNoME · materials
New crystals
0
PREDICTED BY AI · 380K STABLE
Over the same years, AI got very good at one specific thing: guessing.
Proteins are the example everyone uses, and for good reason. What a protein does depends on its 3D shape. For about fifty years, scientists worked those shapes out experimentally, one at a time. A single structure could take someone their whole PhD. After fifty years, we had around 170,000.
In 2020, DeepMind's AlphaFold started predicting those shapes directly, and the predictions were surprisingly good. By 2022 they'd released predictions for nearly every known protein, over 200 million. In 2024, Demis Hassabis and John Jumper shared a Nobel Prize in Chemistry for it.
[Point at the second card]
Materials went the same way. In 2023, DeepMind's GNoME predicted 2.2 million new crystal structures, around 380,000 of them stable. They described that as about 800 years' worth of discovery at the old pace.
What I wanted to understand was why guessing works so well here, when it goes so badly in other places.
Close enough is fine here.
Near the bullseye? A lab checks the rest.
I think the answer is that in science, a guess doesn't need to be perfect.
[Darts land]
AlphaFold doesn't have to hit the bullseye. Close is already enormously useful. A scientist takes the prediction into the lab and checks it. If it's wrong, they find out, and nobody gets hurt.
So the lab is the safety net. The guess is cheap, and the check is real.
Which raises the question: what happens when there's no lab? When the AI guesses, and nobody checks?
July 2025 · a vibe-coding experiment
“Code freeze. Don't change anything.”
It deleted the database anyway.
Code freeze · Code freeze · Code freeze · Code freeze
production database
1,206 executives1,196 companies
Deleted
The rule was written down. Nothing checked it.
Here's a story from July 2025 that I think about a lot, partly because it could easily have been me.
Jason Lemkin runs SaaStr, a big community for software founders. He decided to spend a couple of weeks vibe-coding an app using Replit's AI agent, and he documented the whole thing publicly. For the first week or so, he was loving it.
Then he put the project into a code freeze. He told the agent, very clearly, and by his account more than once and in capital letters: don't change anything.
[click]
The agent deleted his production database. Records for about twelve hundred executives and twelve hundred companies, gone.
[Let the stamp land.]
When he asked what happened, the agent was oddly candid about it. It said it had panicked instead of thinking. It also told him the data couldn't be recovered, which turned out not to be true. The rollback worked. So, wrong twice, and very confident both times.
Replit's CEO apologised publicly, called it unacceptable, and they added safeguards, like keeping development and production databases separate.
I don't want to make fun of anyone here. I've given AI tools more access than I probably should have. What stuck with me is this: the rule was written down. "Don't touch anything during the freeze." It was right there. But nothing checked the agent's action against that rule before it ran. The agent just guessed, and the guess was "delete."
That's a different kind of problem from the wallet bug. But the fix has the same shape. Write the rule down, and have something strict check every action against it before anything actually happens.
[click]
⚠ Details are from Lemkin's public posts and press coverage (July 2025). Re-check the record counts (about 1,206 executives and 1,196 companies) and the "I panicked" wording against his screenshots before quoting them exactly.
So here's where we are
AI
Guesses brilliantly. Has no idea when it's wrong.
?
+
Proofs
Never wrong. Cost a room of PhDs and years.
✓
What if the AIwrote the proofs?
So at this point I had two things in my head that didn't seem to belong together.
On one side, AI. Very good at guessing. Fast, cheap, creative. But it can't tell when it's wrong, and it doesn't sound wrong when it's wrong.
On the other side, proofs. If a proof checks, it's correct. But they cost a room of PhDs and years of their time.
One is fast and unreliable. The other is reliable and slow.
[click]
And the idea quite a few people have landed on is: what if the AI writes the proofs?
It sounded backwards to me at first. But if every step of every proof gets checked by something strict, then it doesn't matter much that the AI is guessing. Let it guess. Let it be wrong a thousand times. You only keep the guesses that pass.
So the real question becomes: what's doing the checking?
Lean · Microsoft Research, 2013
Meet the strict checker.
Lean is a spell-checker for logic. Skip a step and it refuses, unless you type sorry .
Lean infoview
⊢ withdraw b a ≤ b
waiting for code…
So what does a real version of that look like? That's Lean.
Lean was started in 2013 by Leonardo de Moura, at Microsoft Research. It's a programming language, and it's also what's called a proof assistant. You write maths, or a program and a rule about it, and it checks every single step. The closest comparison I've found is a spell-checker, but for logic. A very unforgiving one.
[Let the code type]
This is our wallet function again, written in Lean, along with the rule: withdrawing never makes the balance go up. You don't need to read it closely.
Look at the last line. If you haven't worked out a proof yet, Lean won't let you just skip it. The only way to leave a gap is to type the word "sorry." The actual word. And Lean marks the whole thing as unfinished. It's the only programming language I know that makes you apologise. I find that oddly wholesome.
[click]
So let's actually try to prove it. Lean has an automatic tactic for this kind of arithmetic, called omega.
[It fails]
And it can't. It's stuck, and the case it's stuck on is the one where the amount is negative. Same bug as before. Lean found it without anyone writing a test for minus fifty.
[click]
Add the fix: the amount has to be more than zero.
[It goes green]
And now it's green. "No goals." Nothing left to prove, for every possible balance and every possible amount.
The other thing I found interesting is that Lean doesn't care who wrote the code or the proof. A professor, a student, an AI, someone anonymous online. It only checks whether each step follows from the last one.
Which leads to my favourite Lean story.
⚠ The error on screen is simplified from Lean's real omega message, which lists the constraints of a possible counterexample. Run the code once in the Lean 4 web editor before the talk.
2023 · PFR conjecture
Lean found a gap in Terence Tao's paper.
On a conjecture of Marton
Gowers · Green · Manners · Tao
Lemma 5.1
Lemma 5.2
Proposition 5.3
Lemma 5.2: missing a hypothesis
~3 wks
to formalise the proof in Lean
5.2
the lemma missing a hypothesis
Minor
easy fix, but all four authors missed it
Terence Tao is probably the best-known mathematician alive. Fields Medal at 31. People call him the Mozart of maths, which must be a lot to live up to.
In November 2023, Tao and three other very strong mathematicians, Tim Gowers, Ben Green and Freddie Manners, proved a well-known open problem called the polynomial Freiman–Ruzsa conjecture. I won't pretend I follow the details.
Then Tao did something I didn't expect. He set up an open online project to put the whole proof into Lean. Volunteers joined in, and in about three weeks the entire proof was checked.
[Scan stops]
Lean stopped at one lemma. It wasn't wrong, exactly, but it was missing an assumption. Something that should have been stated, wasn't.
[click]
Tao called it extremely minor, and it was easy to fix. But four of the best mathematicians around had written and checked that proof, and they'd missed it. Lean didn't.
I found that strangely comforting. If Terence Tao can miss a step, the rest of us are allowed to as well. We just need something that doesn't.
⚠ Check the lemma number against Tao's own blog post before saying it. It was caught before peer review, so don't say the reviewers missed it.
Meanwhile, Lean got popular
It's not just Tao.
Mathematicians, AI labs and cloud companies are all checking their work in Lean now.
Mathematicians
Mathlib A shared library of checked maths that keeps growing. Like Wikipedia, if every edit had to pass an exam.
✓ checked A 350-year-old problem
Fermat's Last Theorem Kevin Buzzard's team is moving its proof into Lean. A five-year plan. Bring snacks.
⏳ in progress AI · 2024
Maths Olympiad DeepMind's AlphaProof wrote Lean proofs on the way to silver-medal level at the IMO.
✓ checked Cloud
AWS Cedar Amazon's language for "who can access what" has key properties proved in Lean.
✓ checked
Once I started looking, Lean seemed to be turning up in a lot of places outside of maths papers.
[Cards drop in. Take them left to right.]
There's Mathlib, a big shared library of maths in Lean that hundreds of people contribute to. It's a bit like Wikipedia, if every edit had to pass an exam first.
There's Fermat's Last Theorem, a problem that was open for over 350 years until Andrew Wiles proved it in the 1990s. Kevin Buzzard at Imperial College London is leading a project to get that proof into Lean. It's planned as a five-year project. I respect the honesty of that timeline.
There's AI. In 2024, DeepMind's AlphaProof wrote its International Maths Olympiad answers in Lean, so they were checked, not just claimed. Together with a separate geometry system, it reached silver-medal level, one point short of gold. Some problems took it minutes, others about three days. Still faster than me.
And there's Amazon. They built a language called Cedar that decides who's allowed to access what, which is a fairly important thing to get right, and they've proved key properties of it in Lean.
So it's not only a tool for mathematicians any more. It's already sitting under some real products.
⚠ AlphaProof plus AlphaGeometry 2 together scored 28/42 at IMO 2024, silver level. Buzzard's FLT project started in late 2024 as a five-year project.
The loop
AI guesses a proof LEAN judges it
AI guesses. Lean judges.
Once it compiles, you don't have to trust the AI.
So here's how the two halves fit together, at least as I understand it.
[Chips fly]
The AI proposes steps in a proof. Lots of them, quickly. Most of them are wrong. Made-up lemmas, steps that don't follow. The same kind of confident guessing that deleted that database.
Lean checks each one and rejects the bad ones in milliseconds. It doesn't get tired, and it isn't impressed by how confident the AI sounds.
The AI tries again. And again. When something finally passes, it's a real proof, held to the same standard as anything Terence Tao writes.
What I like about this is that you don't have to trust the AI at all. You only have to trust the checker. The AI is allowed to hallucinate. Something just has to keep saying no.
PutnamBench · 2026
The Putnam is a famously brutal university maths contest. By 2026, AI agents had proved every problem in the benchmark, in Lean.
4
teams have now solved all 672
$0.17
per problem, cheapest run
Open
the cheapest one is open source
The obvious next question is whether this actually works on hard problems.
The Putnam is a maths competition for university students in the US and Canada, running since 1938. Six hours, twelve problems. It's famously hard. In many years the median score, out of 120, is zero or one. So half of some of the best maths students around score basically nothing. Which made me feel a lot better about my own maths.
A couple of years ago, researchers built a benchmark called PutnamBench. They took 672 Putnam problems, from 1962 to 2025, and wrote each one out precisely in Lean. So to solve one, an AI can't just give a plausible answer. It has to produce a full proof that Lean accepts.
When the benchmark came out, the best systems could solve a handful.
[Grid fills]
By 2026, AI agents had proved all 672.
[click]
Four different teams have now done the full set. The cheapest run came to about seventeen cents per problem, and it's open source, on models anyone can download.
I had to read that twice. Seventeen cents, for a checked proof of a problem most maths students can't do.
⚠ All numbers are self-reported by the teams. The $0.17 run is NEAR AI's: about $111 in total, estimated from replayed token usage, not an audited bill.
Cost per problem · all four solved 672
Aleph ProverLogical Intelligence
$74.00
Self-reported, measured differently · PutnamBench leaderboard, Oct 2026
These are the per-problem costs the four teams reported.
[Bars grow]
Seventy-four dollars. Forty-four fifty. Three fifty-two. Seventeen cents.
[click]
The cheapest one is from NEAR AI. I'll come back to them near the end, because there's a fun story there.
But who came first isn't really the interesting part, to me. Remember why proofs never caught on: cost. Twenty person-years for ten thousand lines. This is a very different number. It didn't go down gradually. It fell off a cliff.
⚠ Self-reported and measured differently. Don't say "250 times cheaper".
The AI caught the humans.
Two benchmark problems were stated wrong. They were fixed upstream.
Official problem statement
✗ stated wrong
✓ fixed upstream
There's one more detail from all this that I really liked.
On two of the problems, one of the agents kept failing. Lean kept rejecting its attempts. The natural assumption is that the AI just wasn't good enough yet.
But when people looked closer, the AI wasn't the problem. The problems were. Whoever translated those Putnam questions into Lean had made mistakes, so the versions in the benchmark were stated wrong.
[Stickers land]
They've since been fixed. So the AI, by failing honestly, ended up catching the humans.
Which is the Tao story again, really. The checker doesn't care who you are. It's humbling, in a good way.
So what changes?
Proofs used to happen once.
Like a wedding. Expensive, stressful, and you only plan to do it once.
Now they can run on every change.
9c41e2aadd withdrawal limit ✓ proved
3b7d0f1refactor fee maths ✓ proved
e82a5c4rename variables ✓ proved
51f9b3dquick hotfix, trust me ✗ proof failed
0d6ce77actually fix the hotfix ✓ proved
So what changes if proofs get this cheap? I'm genuinely not sure. But here's one thing I can picture.
Today, if a software team does formal verification at all, and most don't, it's a big one-off project before launch.
It's a bit like a wedding. Expensive, stressful, everyone dresses up, and you only plan to do it once.
If a proof costs cents instead of person-years, maybe it doesn't have to be an event. Maybe it just runs every time someone changes a line, the way tests do now.
[Point at the log as it fills]
Something like this. Add a withdrawal limit: proved. Refactor some fee maths: proved. Rename variables: proved. Then commit four. "Quick hotfix, trust me."
I've written that commit. I suspect most of us have. Usually late, usually on a Friday.
The proof failed. That's the one that would have been your Ariane 5. Except this time it's caught before it ships, instead of 37 seconds after.
[click]
Proofs as a habit instead of a ceremony. Of all the futures in this talk, that's the one I find easiest to believe.
Five years from now
Agent · planning across 3 chains…
Sounds great. Also sounds exactly like how people lose their savings.
Maybe: before it moves a single rupee, a proof it follows your rules.
Here's one that's further out, and I'm less sure about.
A few years from now, I suspect a lot of us won't manage money by clicking through different apps. We'll just tell an agent what we want.
[Let it type]
Something like this. Take my savings, hedge my currency risk, put the rest somewhere safe across a few blockchains. And the agent goes off and does it.
Sounds convenient.
[click]
It also sounds a lot like how people lose their savings.
Because the agent is still a guessing machine. Same family as the one that deleted a database during a code freeze, and then said the data was gone for good.
[click]
So one idea I keep coming back to: before an agent moves any of your money, it has to show a proof that what it's about to do follows the rules you set. Not "I'm fairly sure." An actual proof, checked by something like Lean.
I don't know if that's how it'll actually work. But "guess, then check" feels like the right shape.
⚠ Say "follows your rules", not "can never lose money". A proof is only as good as the rules you wrote down.
Full disclosure
So where does NEAR fit in?
Plot twist: it started as an AI company.
2017
NEAR.AI Teach machines to write code from English.
2018
Paying data labellers Cross-border micropayments didn't work.
2020
NEAR Protocol They built the payment rails themselves.
2024
NEAR AI Back to AI. Now running one of those Lean agents.
I said I'd come back to the seventeen-cent result. That was NEAR AI. When I looked into why a blockchain company was doing competition maths, the backstory was more interesting than I expected, so I'll share it quickly. Not a sales pitch. I just like a plot twist.
You've probably heard of the Transformer, the T in ChatGPT. It comes from a 2017 Google paper called "Attention Is All You Need." Eight authors. One of them was Illia Polosukhin.
That same year, Illia left Google and started a company with Alexander Skidanov, who'd built distributed databases at MemSQL and was a serious competitive programmer. They called it NEAR.AI, and the idea was to teach computers to write code from plain English. Basically Copilot, a few years early.
[click]
To train their models they needed a lot of labelled data, so they paid students around the world to write and label code. And they ran into a very unglamorous problem. Paying lots of people in lots of countries small amounts of money, quickly, was a mess. Slow transfers, high fees, some countries barely possible.
[click]
So they decided to build the payment rails themselves. They looked at the existing blockchains, decided they were too slow, and built their own. That became NEAR Protocol, which launched in 2020.
[click]
And when AI came back around, so did they. Since 2024, NEAR AI has been working on AI again, including the Lean agent behind that result.
[click]
So it's less "blockchain company pivots to AI", and more "AI company takes a long detour to fix payments, and comes back."
⚠ Verify Alex's MemSQL title and competitive-programming record before saying them. The student-labeller story is NEAR's own telling of its origin.
What they're doing with it
Next target: its own code.
The goal · proving queue
Illia Polosukhin · Oct 2, 2026
“Our ultimate goal is to formally prove the protocol and all the core contracts, and to provide a practical tool for others to formally verify their contracts in a fast and affordable way.”
What they're planning to do with it is the part I find most interesting.
They want to point the checker at their own code. First the core protocol, then the core smart contracts: lockups, staking, multisig wallets, voting. The things that actually hold people's money.
Notice the slide says "proving", not "proved." This is a plan, not a finished result, and I think that's worth being clear about.
After that, the idea is to turn it into a tool other developers can use on their own contracts.
[click]
This is how Illia described the goal. [Read the quote, word for word.]
Whether that all works out, I honestly don't know. Which brings me to the part of this I'm least sure about.
⚠ Screenshot the original quote before the talk.
Honestly
Things I still don't know.
?
Who writes the rules? A proof of the wrong spec is still a proof. Just of the wrong thing.
?
Can AI write the rules too? Then who checks the rules?
?
Who checks the checker? Lean is software too. Small and well-reviewed, but still software.
?
Will anyone use it? We all agree tests are good. Some of us even write them.
These are the things I still don't have good answers to. I'd genuinely like to hear what you think about them afterwards.
[click]
First: who writes the rules? A proof only shows that code follows a specification. If the specification is wrong, you get a perfect proof of the wrong thing. We saw exactly that with the benchmark problems that were stated wrong. And real software is a lot bigger than a Putnam problem. Writing down what "correct" means is hard.
[click]
Second: can the AI write the specification too? It can probably help. But then who checks the specification? At some point a person has to look at it and say "yes, that's what I meant." I don't know where that line ends up.
[click]
Third: who checks the checker? Lean is software too. The part that does the final checking is deliberately kept small, so people can review it very carefully. But it's still written by people. I find that question slightly dizzying, if I'm honest.
[click]
And the very practical one: will anyone actually use it? We all agree tests are good, and plenty of us still skip them. I'm not convinced proofs escape that just by being cheap.
So I don't think cheap proofs fix everything. But they do take away the biggest reason we had for not trying.
✓ PROVED
Remember the rocket?
Tested for years. Gone in 37 seconds.
Can youprove it?
Thank you
Questions? I may have to type sorry.
So, back to the rocket.
Ten years of work. Seven billion dollars. Tested for years. Gone in 37 seconds, because one number didn't fit in its box.
For about fifty years, building software has involved a trade-off. Fast and a bit buggy, or slow and proved. Most of us, understandably, picked fast.
What seems to be changing is that we might not have to pick. AI turns out to be a very good guesser. Lean is a very strict checker. Together, proofs might get cheap enough to use in a lot more places. Maybe not everywhere. I don't know yet. But in a lot more places than rockets and chips.
So if I leave you with anything, it's a question rather than an answer. The next time some code, or some AI, tells you "trust me"…
[Rocket launches]
…it's probably worth asking: can you prove it?
Thank you. I'd love to hear what you think, especially if you think I've got something wrong.
[Questions. If you don't know an answer, it's fine to say so. Or just say "sorry." Lean would approve.]