# Formal verification could make AI-generated tools trustworthy

Markdown copy of https://realalpha.app/s/formal-verification-could-make-ai-generated-tools/ on Real Alpha, the best minutes from long interviews with the people building AI. Cite and link the page, not this copy.

- Speaker: [Max Tegmark](https://realalpha.app/people/max-tegmark/) · Max Tegmark is an MIT physics professor, cosmologist and author.
- Host: [Brian Keating](https://realalpha.app/people/brian-keating/) · Host, Into the Impossible With Brian Keating
- Show: Into the Impossible With Brian Keating
- Episode: [Max Tegmark: We’re Building A Replacement Species](https://realalpha.app/v/nnYHg0gcWug/), Oct 23, 2026
- Moment: 48:09 to 52:31 of the episode (4 min), playing on https://realalpha.app/s/formal-verification-could-make-ai-generated-tools/; the episode from there: https://realalpha.app/v/nnYHg0gcWug/?t=2889

## Quote

> “So it's like VibeCoding, except you have an actual **machine-checkable proof** that your tool now does what it wants.”
> — [Max Tegmark](https://realalpha.app/people/max-tegmark/) at [49:12](https://realalpha.app/v/nnYHg0gcWug/?t=2952) · Into the Impossible With Brian Keating

## Takeaways

1. AI could generate code in languages such as Python, Rust, or Lean.
2. A proof can verify that a tool does what it is meant to do.
3. Tegmark conjectures that smarter AI may export nearly all its knowledge.

## About this segment

Max Tegmark proposes having AI turn its discoveries into code with machine-checkable proofs. If smarter AI can export more of its knowledge this way, critical tools need not rely on black-box models.

From “Max Tegmark: We’re Building A Replacement Species”, Oct 23, 2026. [Watch the full episode](https://realalpha.app/v/nnYHg0gcWug/)

## Transcript

Transcribed by machine (Whisper) from the episode’s audio, so a word may be off here and there.

[48:16](https://realalpha.app/v/nnYHg0gcWug/?t=2896) mathematicians the terence tau and and others in uh at the and and jacob simmerman and others at ucla so i was talking about how where we are now is we have ai that we cannot trust enough swarms break out of open ai and anthropic and go hack and all sorts of bad things happen what we all want is controllable tools yes and there's the traditional way to try to get controllable tools is to try to understand the artificial neural networks we're working on I have worked for years and mechanistic interpretability etc many are trying that I think it's gonna be too little tote too late even though it's scientifically it's just so much fun but there is a different path to get there which is much easier and actually much faster which is you ask the AI that has figured out also the cool algorithm and tools to code this up for you and

[49:12](https://realalpha.app/v/nnYHg0gcWug/?t=2952) in a language like Python, or Rust, or Lean, and then give you a proof that this tool does exactly what you want. So it's like VibeCoding, except you have an actual machine-checkable proof that your tool now does what it wants. I call it VeriCoding, V-E-R-I coding, Formally Verified Coding. And I have a conjecture I want to end by sharing, which I call the asymptotic internal transparency conjecture and if it's true we can have an amazing future so imagine the nerd plot we have on the x-axis intelligence and on the y-axis the fraction of the algorithms and knowledge that can be actually exported into computer code and proven So, for example, the conjecture first says that this curve is increasing.

[50:05](https://realalpha.app/v/nnYHg0gcWug/?t=3005) You know, a mouse that's learned a new cool algorithm for finding cheese or something can't code that. It has 0% exportable fraction because it can't even program, right? You can. If you, Brian, figure out a new way of operating this new future CMB polarization satellite, we could if we were doing it the way the industry is doing it now what we would do is put you in the satellite with with a lot of food and some oxygen tanks and say okay steer the satellite brian and then if someone is like i don't know can we really trust that he's still gonna function after two years there you know well let's do neuroscience on brian's brain figure out how brian's brain works smart uh this is clearly the better way we would just say hey brian you know i think your exportable fraction is pretty high why don't you just take this

[51:02](https://realalpha.app/v/nnYHg0gcWug/?t=3062) algorithm that you invented with your neural network and export it into python or lean or something and give us a proof that it's going to do exactly what we want and then we launch the computer in the satellite instead so you can hang out here at home on earth with your kids and the satellite is going to work great right what i'm saying is and here comes the conjecture the asymptotic internal transparency conjecture says not only does this can smarter neural networks artificial neural networks export more of their knowledge but it asymptotes the 100 percent so in a future super intelligence or a very very smart ai that has access to all its own weights It's all its own activations, you know, the way a human neuroscientist can only dream about.

[51:47](https://realalpha.app/v/nnYHg0gcWug/?t=3107) We'll be able to figure out enough about its algorithms that it's learned that it can actually export it into traditional provable computer code. If this is true, it's amazing because we no longer need to deploy our black box neural networks. we can put them in an air-gapped room somewhere and then all we need to deploy are always this traditional but formally verified computer code that you can by definition trust because you can prove it so that's a happy note for me that's right me is and it's feasible you know you know we don't even have to figure out how the AI works you can code in Python even though I don't understand