Vlad Tenev, co-founder and CEO of Robinhood, started from a simple piece of arithmetic. Human-written software already has bugs and security holes, he said on Moonshots with Peter Diamandis. If AI can write a hundred times as much code as a typical person in a day, you should expect the number of defects to grow with it. Some of those bugs, he added, "will just be bugs that have catastrophic consequences", even when the intentions behind the code are good. He pointed to cryptocurrency, where a flaw in a smart contract (a program that holds and moves money automatically) can let "hundreds of millions of dollars" be drained "instantaneously".
His proposed remedy is formal verification: proving mathematically that a program does what it is supposed to do, rather than testing it and hoping. He said Harmonic, a company that host Peter Diamandis had brought up earlier, was "created to solve this problem". The goal, he said, is "a firm grounding through formal verification" that the AI "is doing the right thing."
The episode was published on September 19, 2026. The discussion turned into a debate about what such a guarantee covers and what it leaves out.
The proposal: code that carries its own proof
Tenev's model example came from mathematics. Anthropic had recently published a formalization of Fermat's Last Theorem. It runs to about 13 million lines of Lean, a programming language in which every step of a proof must follow from earlier steps by rules the software enforces. Tenev set this beside the theorem's human history. When Andrew Wiles first announced his proof, it took people months to read and understand. Then someone found an error, and it had to be repaired before a panel of mathematicians accepted the proof. (Tenev's timeline is longer than Anthropic's. The report dates the first announcement to 1993, says the repair took about a year and puts publication in May 1995.)
"AI producing a 13 million line proof. No human's going to read that," Tenev said. "How do you know that it's correct?" He called this the same problem as asking whether software does the right thing, or whether a chip's behavior "matches your specification". His answer is a certificate. Lean, he noted, can apply mathematical proof techniques to programs as well as to theorems. He predicted that AI-generated code will increasingly come "with a certificate that makes it really, really easy to verify without reading the code that its behavior satisfies the properties that you want it to satisfy."
Three separate jobs: producing a proof, checking it and checking what it says
The proposal is easier to judge once three jobs that often get blurred together are separated.
Producing the proof. This is the creative and expensive part. For the Fermat run, Anthropic's agents worked for eleven days, and the successful run used about six billion output tokens (the chunks of text a model generates). Harmonic's Aristotle system combines informal mathematical reasoning with a search for proofs in Lean. It proposes intermediate steps called lemmas, and feedback from Lean helps it revise proof sketches that fail. An earlier article covered how the Fermat proof was produced. Under the certificate idea, nobody has to trust whatever produced the proof, because the checker does the judging.
Mechanically checking the proof. Lean's kernel, the small core of the program that accepts or rejects each step, checks the finished proof. The check relies on a few axioms, the foundational assumptions everything else is built on. Anthropic reports that Lean checked the Fermat proof using its three standard axioms. Lean's reference manual describes sorry, a placeholder that stands in for an unfinished proof. A file that contains it can still be processed, and Lean only prints a warning. So "it compiles" does not mean "it is proved". Listing the axioms a theorem depends on shows whether it quietly relies on the assumption behind that placeholder. Aristotle's authors use a similar standard. They count a problem as solved only when there is a complete Lean proof with no gaps or unsound assumptions.
Checking that the statement is the right one. A perfect proof of the wrong claim does not guarantee what you care about. For Fermat, Anthropic says a separate comparator confirmed that the final statement matched the formulation in Mathlib, Lean's shared mathematics library. In Harmonic's 2025 International Mathematical Olympiad evaluation, humans translated the six problem statements into Lean inputs, and the later formalization of lemmas was automated. Aristotle solved five of the six problems, a result equivalent to a gold medal, but it did not solve the last one.
The debate on the podcast centered on this third job.
The objection: an AI can prove the wrong thing
Alexander Wissner-Gross, a computer scientist and the founder of Reified, raised what he called "an elephant in this particular room". You can "spec it, you can certify it all day long," he said. But unless you are very careful with definitions, a model may "subtly define things" so that "it's actually solving a different problem than the one you're solving." He asked Tenev whether Lean-style autoformalization (AI translating ordinary statements and proofs into Lean) could help with strong AI models misbehaving in sandboxes, the restricted environments where they are tested, without falling into the same trap.
Tenev first acknowledged the edge cases. People can change Lean's axioms, and "if you change the axioms, then you can prove all kinds of weird stuff." In theory the kernel itself could also have a soundness bug. Wissner-Gross granted the kernel's soundness, saying the Lean 4 kernel had been "studied to death". His worry was the millions of generated lines around the core statement: "did it actually define everything correctly? Or is it somehow subtly inserting cheats or definitions?" He put the sharpest version as a question: "How do you avoid the problem of a strong AI sneaking in helpful to it definitions that are harmful to the humans?"
Tenev's reply relied on how small the part you have to trust is. The statement of Fermat's Last Theorem is "one very simple line of lean", he said, plus one line of things it depends on. A person reviews that and does not have to check the 13 million lines of proof, "where the bulk of the work is." He said models are also formalizing statements more faithfully. They "used to make terrible mistakes," such as changing addition to subtraction, and now do so less often. Even if the process is imperfect, he estimated that it "probably saves you" more than 90 percent of the effort, "and probably way, way more."
He also cited the de Bruijn factor, which he described as the reason mathematicians have not formalized their work: until recently, formalizing took 10 to 20 times the effort of writing a proof on paper. He argued that working formally may already be faster, because mathematicians can check lemmas as they go. He said mathematics is "going through that transition as we speak."
Wissner-Gross granted that mathematics suits this approach but explained why the approach may not carry over. Fermat is "easy to state, but hard to prove", and such problems are "the catnip for auto formalization." You check the short statement by hand, trust Lean for the rest, confirm that the proof contains no sorry placeholders and declare victory. "But with like real world safety, it's not obvious to me at all," he said. He said he did not know how to state "this AI is going to behave safely in a general purpose environment" concisely enough for a person to audit it and say, "yep, this is a correct statement of safety."
Tenev's answer: verify small pieces and build upward
Tenev did not claim to have a short statement of safety. Asked whether AI model behavior itself will be formalized, he said: "I guess I'm not sure." He pointed instead to deterministic systems, which always give the same output for the same input, and whose properties are easier to state. Chips were his example. You don't want a chip to "freeze and halt", so you prove liveness, the guarantee that the system keeps making progress. You also prove that certain operations finish within "10 or 20 clock cycles".
His method is decomposition. Start with a small submodule and prove its properties, such as its liveness, how long it takes to do something, or that its adder (the circuit that adds numbers) works. Bigger modules are built from submodules, so as models become more capable you move up "one level of abstraction". He compared this with mathematics, which progressed from verifying small lemmas to verifying Fermat. He said a human project to formalize Fermat, "out of Imperial", had been slated to finish by 2032.
His timelines are forecasts. He expects AI-assisted verification to cover the entire Linux kernel "in a couple of years", or "maybe even less at this rate". He said all mission-critical software and all hardware will "almost assuredly" be formally verified with AI's help. He also said he "would bet" that verification will find its way into LLM and AI model behavior "in some form or fashion within the next five years."
Wissner-Gross named the assumption underneath. Achieving real-world safety through autoformalization, he said, seems to require being able to "hierarchically decompose the real world into provable sub worlds." Tenev agreed: "Absolutely."
A different kind of trust: testing and measured risk
Dave Blundin, founder and general partner of Link Ventures, welcomed the certificate idea but described a looser kind of guarantee. He said that language models give the same answer to the same prompt but can shift sharply if "even one character or one space" changes, and he compared this to chaos theory. His example was Tesla's self-driving software. He said Elon Musk describes it as having moved entirely to neural networks, so in theory it "could in theory do anything at any given moment". In Blundin's view, it has been "so tested and so beaten to death" that it is far safer than a human driver.
He said the certificate is "beautiful as a concept" because it is not "a guarantee of exact input output". That is impossible, he said, because the possible combinations are nearly infinite. Instead, it would show that a system is "bounded or it's contained or it's below some risk level." Later he suggested measuring how far a model's output moves when its input is tweaked. He compared this to a person who is rational 99 percent of the time but "really off" otherwise. That deviation could also be measured and bounded, he said, and "there's probably 10 other approaches we're not thinking of". Together, he argued, these could certify systems as safe or not safe.
This claim is different from Tenev's. A Lean proof that a circuit meets a timing bound covers every case included in its statement. Blundin's approach rests on extensive testing and measured deviation from expected behavior, which is evidence about risk rather than a proof.
The idea also relates to a distinction Blundin made earlier in the conversation, between using AI to write fixed rules and letting AI make live decisions. A certificate fits the first case most naturally, because code that has been written down can be checked before it runs.
Open questions
- Who writes and audits the specification? Fermat had a short, widely accepted statement. In the Olympiad evaluation, humans formalized the problems. For software, and especially for AI behavior, Wissner-Gross doubted that a statement of safety could be short enough for a person to check.
- Does safety break into pieces? Tenev's approach works when a whole system's properties follow from its parts' properties. Wissner-Gross's question is whether "safe in a general purpose environment" can be built up that way.
- What counts as a finished proof? Placeholders such as
sorry, added axioms and definitions all have to be inspected. A certificate is only as strong as its checked assumptions. - Will the forecasts hold? Verifying the Linux kernel within a couple of years and verifying model behavior within five are predictions. On the question of formalizing model behavior, Tenev said he was unsure.