ɛ∞ɜɛ∞ɜ

2. Formally Verify All Software

October 31, 2026 · 00:29:32

Read this as a blog post →

Mastered, transcribed and published by AI using these skills.

The second episode of the Millillion podcast.

Jordan Last (lastmjs) announces Lasm, his recently launched project that allows Lean to run almost anywhere that JavaScript or WebAssembly runs today. First he explains why building correct software is so difficult, and how formal verification lets you prove that certain properties hold for all inputs.

Lasm on GitHub: github.com/Millillion/lasm

Transcript

[00:11] All right, everybody, welcome back to the next episode of Millillion, or the Millillion podcast, actually. This is Jordan, also known as lastmjs. Today I want to talk to you about my recently launched project called Lasm, spelled L-A-S-M. Lasm, that word, or that name is a combination of the name of the amazing programming language Lean, spelled L-E-A-N, and the amazing portable bytecode format WebAssembly, which is shortened to Wasm, W-A-S-M, together, Lasm.

[00:58] Now let’s just talk a little bit about what’s going on here. Let’s just talk about software development in general. Software development is very difficult. Why is it difficult? Well, you’re producing tons and tons of code. If you’re not familiar with code, you basically write out lines upon lines upon lines of instructions. So imagine a book or a blog post or something. Each of those lines is telling something to a human. It could be instructions, it could be persuasion, it could be just general information.

[01:47] Generally speaking, when you’re writing computer code, every line or statement is a specific instruction that’s telling the computer to do something. And to create the software that runs our lives, I mean, software in many ways is running many or most aspects of our lives. Whenever you interact with, I would say, probably most machines, there are computers processing to make this stuff all run safely and securely. So the problem with generating so much code, the problem with the amount of complexity that we’ve created to make these machines run our lives and make our lives better and…

[02:36] …more prosperous if we use these things correctly, in my opinion. The problem with this absolutely outrageous amount of complexity is that it’s complex. And complexity is hard to manage and hard to tame. The more moving parts you have, the more pieces that need to fit together in certain ways, just the more complicated something is, the easier it is for that thing to fall apart if we don’t understand it very well and basically build it correctly. So building correct software that always functions exactly as we desire it to function is very difficult.

[03:26] I think everyone kind of knows this. In our apps, in the software that people use on a regular basis, we know of the term bug. Things are buggy. There are bugs in all kinds of things. And it’s kind of annoying when that happens. Sometimes it’s just annoying. Like, oh, this, I don’t know, my Instagram app or Twitter app, there’s some little thing wrong with the UI or something. That’s okay. It’s not too bad. But what if it’s something with your bank account or bank balance? Okay, that’s a little bit more worrisome, right? Like, if balances are wrong or something, you really need to go get that fixed. What if you have a medical device running inside of your body? Like a pacemaker or something like that, right?

[04:16] What if you’re in the middle of a surgery? And the only reason the surgery is possible is because of machines including computers. So software, writing correct software or writing software and verifying its correctness is incredibly important. Absolutely vital. And you know, it depends on the type of software that we just discussed, like you don’t need absolute assurance for everything. And it might be impossible to have, I mean, the amount of absolute assurance that you can have, I guess is what we’re about to talk about. But generally speaking, to make your software correct, in the age before AI, at least, and…

[05:04] …a lot of these concepts do flow into the world of using AI agents to write software, a lot of the techniques that we’ve used in the past are, well, let’s just go through them. So first off, you have the original human mind that is reasoning through the code. Usually I’d say software engineers don’t try to write code that is wrong. So the human engineer uses their own cognition, their own intellectual power to come up with a model in their mind of what’s happening or what should happen when their code runs. And these models, generally speaking, are incomplete and flawed.

[05:51] So what we do is we basically do our best. Like if you’re just a software developer engineer, you know, writing out to some program, something that you’re doing, you go for it with your absolute best, you do your best thinking, you review it multiple times, you really clean it up, like you do everything you can yourself before you say like, okay, this is now ready according to me, but what does ready mean? Usually if you’re doing it right, like this is how I’ve done it at least. Usually once you personally have done it correctly or once you’ve personally have finished and believe that you have done it correctly, then you create a pull request. Usually I love Git, I love GitHub. So you make a pull request with the code that you’ve created.

[06:38] So you know, this could be something small, like just a few files and a few hundred lines of changes to something absolutely enormous, like at least back in the day, 50 files, 100 files, 300 files, like that’s getting pretty huge for a PR with who knows, like into the thousands of lines changed, added, removed, or just changed. So yeah, so you make this PR and then what you do is you ask another cognitive being, so another human on your team, you ask that human, hey, can you review my PR? And this is like built into the engineering process, like usually it’s not like, oh, hey, can you do this?

[07:23] It’s like, you must do this. This is part of how we work. So you usually have an independent human software engineer review your work. And what’s nice is that human has to come up with their own independent model of what’s happening and, you know, their biases and their software upbringing and their life experience, it’s different. Every person has a different brain, right? And so they bring different strengths and weaknesses. And so that usually helps to wring out even more bugs as you think about things from different angles. And then, great, so you do multiple independent reviews. That’s like pretty standard. But also as part of the code you write, you usually write tests. You write test cases.

[08:11] And there’s all, there are many, many different methodologies for testing software. But the core concept is that you write a small program that executes the program under test and then looks at its result and then checks that the result is correct. So you make a program that calls the program and then verifies the result of the program. And the simplest form of testing is probably example-based testing, where you basically just come up with an example. Let’s say the program you have just to be simple. Let’s say it’s just a little function that calculates the age of a user based on their birth date.

[09:03] So like you have a function. It takes as a parameter the birth date of a user and then returns the age of the user as like a number or an integer or something. Okay, cool. So what would an example-based test look like? Well, you would say, okay, you maybe contrive a user who was born in 1996. Let’s say they were born in October, on Halloween, I’m recording this on Halloween. They were born October 31st, 1996. All right, what do you expect that function to return? It should return 30, right?

[09:48] Because it’s been 30 years. That person would be turning 30 today, right? I believe so. Hopefully there’s not an off-by-one either. So then you, boom, there you go. That’s your example test. You would write a function that says, all right, create this user or create this birth date. It’s 1996. Okay. So if we calculate age function, pass in that birth date, it will calculate the age and return it. And then you’ll check in your example-based, you know, basically like a unit test, right? You’ll check in your example-based test if the result is 36. Boom, that is one example-based test.

[10:34] And this testing is used quite a lot. I guess I can’t say, like, generally speaking, but for most testing I’ve seen in like open source projects, et cetera, like, example-based tests are used quite a lot. And they’re just a one-off example, like, one-off example test this, one-off example test this. I mean, you might cluster one-off examples in a certain area, but there’s a lot of example-based testing out there in my experience. And hopefully you can see that it’s a little bit limited, like, all you’re doing, you’re trying to prove that your functionality is true or is correct no matter the input that comes into it.

[11:21] Like, for all inputs, this certain behavior holds. The problem is with example-based testing, you’re never actually proving that. Like, you’re not mathematically or logically able to say this is correct under all possible inputs or conditions. You’re just generating evidence, like, all right, I have evidence that this one example works. Okay, now you have, let’s say you do 10 examples. I have evidence of 10 examples. And let’s say you do 10 more examples trying to think of weird edge cases. Okay, now I have 20 examples and some of them have edge cases. Okay, that’s fine. That’s getting better.

[12:08] We’re gaining more confidence that this function is correct. But we really don’t know. There’s no proof here. We don’t have a proof. We have evidence. No mathematical proof, no logical proof, just evidence. So then what? So then, what would be the next step? How could we make this even better? Well, let’s continue down. We’re trying to prove this. We want mathematical proof, like, you can look at some kind of code or some kind of proof or something, some statement saying this is correct for all inputs. That’s what we want. But we only have these 20 examples. Well, can we just generate more examples?

[12:55] Yeah, you can always generate more examples. The problem is that takes a lot of human effort. Okay, yeah, we have AI. Sure. But even with AI, like, you will never generate infinite examples because that’s not possible to do. Even with AI, you cannot generate infinite examples. So, all right, so what if we then, instead of one example, like an actual written out example, test case per example, what if instead we thought like this? What if instead we generated, we created like some kind of object or function that can actually generate random inputs of the shape of the parameter of the function under test?

[13:41] So imagine this, just think of this for a second. Our test is called calculate age, and remember, it takes a date as an input. The date is the birth date, the birth date as the input. Okay, so what if we created like a function that generates random birth dates? It can generate random birth dates from 4000 BC to 2026 or any birth date, way back like just millions of years to millions of years in the future or something, right? Like the entire possible set of birth dates. Okay, now, with this random function, let’s say we randomly generate one of these things. And in a loop, basically, in a loop, we say, generate a birth date, call the calculate birthday function, come back.

[14:30] And instead of checking that that example is correct, because you can’t check that the example is just correct, like hard coded, because we’re trying to get away from that. What if you instead check properties that should hold? Okay, like claims or propositions that should hold whenever you’re calculating a birth date. So let’s think of a couple of these. So the age of a person should never be negative, right? That doesn’t… Well, okay, okay, yeah, yeah. So if a person was born, then yeah, we’re saying that there’s no negative ages here. We’re saying that age is from when you’re born and on.

[15:16] So one property that should hold for all inputs is that the age never is never less than zero. Boom, that is a property we could put in it as a claim that we can make or proposition that should hold for all inputs. Now with this random generator, we can generate millions and billions of inputs really cheaply. Now we’re still just creating evidence. We still do not have a proof, but now look, we have like this random distribution and we can generate way more evidence. So we can start to emulate a mathematical proof. We can emulate trying to get as close as possible to proof that all inputs are always going to be correct. But it’s asymptotic.

[16:01] We’ll never actually get there. We will never get there. And there’s still not enough computational resources to execute this thing for that long. Okay, so then what’s next? What is the next step? And you could think of other properties. I don’t know off the top of my head. I don’t want to keep thinking about it, but you basically just think of all the properties that should hold and then you execute the generator. That’s called property testing or property-based testing. I love property-based testing. It’s really awesome. But there’s something better. There actually is a way to mathematically prove that for a certain function, it behaves correctly under all inputs. Sorry, that behaves correctly.

[16:51] What I’m actually saying is that certain properties hold for all inputs. And that is called formal verification. Formal verification, I guess I’m not like an expert in formal verification, but to me, it is an amazing concept that I’ve followed for years. And I’m now really diving into it because AI now makes it practical to begin to formally verify software that would just be outrageously difficult to formally verify before. And so, sorry, I was trying to define formal verification still. So formal verification basically allows you to provide the mathematical proof that certain properties do hold under all inputs.

[17:42] And with enough cognitive effort, hopefully you can come up with a set of properties or a set of propositions that are individually necessary and collectively sufficient to characterize the intended behavior of your functionality. I think that is the core thing to understand. And I mean, this would be absolutely just amazing if all of our software, not just crazy mathematical calculations, not just cryptographic primitives, not just like TCP, not low-level protocols, no, not just that, but imagine being able to formally verify front-end code like HTML and CSS and JavaScript and SQLite and Postgres back-end code as well, HTTP endpoints, reading to the file system.

[18:43] What if we could formally verify all of that? That is my dream. And with AI, that becomes a possibility. I believe that with AI, what was previously impossible or seemingly impossible or impractical is now possible. That’s how we need to think about it now. The task that just seemed outrageous before, that’s where we need to set our sights. The easy tasks from before are now trivial. The hard tasks from before are now easy. The impossible tasks from before are now hard. In some ways, they’re kind of easy, actually, because of AI. But now let’s go after that.

[19:29] So formally verify all software. I feel like that is now my mantra. That’s what I’m after. I want to formally verify all software. And that’s just going to be crazy. So how would you do this? There are certain languages and tools and techniques that allow you to formally verify things. And my favorite is called Lean, L-E-A-N, Lean. Lean is a general purpose programming language. It’s also a functional programming language, which I’m in love with functional programming. I have been for a long time. But I’ve never really tried to adopt a truly functional programming language because I just feel like it’s been impractical, like Haskell and F# and things. They’re not super mainstream. And I preferred to stay in the mainstream with TypeScript and Rust, TypeScript and Rust and things like that.

[20:20] So the next, but Lean is amazing because it is a general purpose functional programming language with formal verification built in. You can write functions in the Lean syntax. And you can prove propositions about those functions right there in the Lean code. It is in the same language. Now, that is powerful. That is amazing. I don’t know if you’ve seen, but the major AI labs have been heavily using Lean to prove crazy mathematical things. Formal verification is in some ways exploding right now, becoming much more popular.

[21:07] This is starting to spread. And I think this is really the next evolution of software engineering and programming languages, is moving to formally verify everything. And this is going to allow us to generate massive amounts of code, much more code than we’ve ever had before, and allow the AIs and the humans to ensure that it is correct. I think this is possibly the only way that we can move forward and scale the amount of code that we’re generating. And personally, what I’m super excited for with adopting Lean is like my test cases at work, like these test suites are just growing. And they take like 20, 30 minutes.

[21:55] They take a long time to run. And I’m hoping that I can shrink that a lot with just a compilation check with Lean. I didn’t say that before. With Lean, you write a proof. So you write propositions, you write a proof, and you combine that with a name into a theorem. And Lean will check it for you automatically. It will check the proof. And if it doesn’t compile, then the proof is wrong. If it compiles, the proof is right. So you can basically have AI generate the proof in whatever way. The proof doesn’t have to be pretty, doesn’t have to be nice. And you know that the proof is correct, more or less. There could be bugs in the Lean, proof checking kernel, and things like that. And then you can also have the AI reason about the claims, which are the prop type or the proposition type in Lean.

[22:42] You can have the AI reason about those claims. And I feel like it’ll probably do a pretty good job. But that’s possibly an area where human expertise is maybe still very valuable. But whatever, it doesn’t matter. We’re heading towards being able to formally verify, hopefully, all software, at least much more software than before. Now, finally, with that introduction, I want to announce my project Lasm. Lasm allows Lean to run. Almost anywhere that JavaScript or WebAssembly runs today. So that means in the web browser, in Node.js, on serverless platforms like Netlify, Vercel, Cloudflare, Cloudflare Workers, and edge platforms.

[23:35] So yeah, the edge platforms like Cloudflare Workers and other edge platforms. And we have some Bun and Deno support as well. I don’t remember exactly the extent to which, but it’s very extensive. I have been pushing the AI to very thoroughly test and ensure that we have support for many, many platforms. And this project is now launched. You can go to the Millillion GitHub organization, and you’ll find Lasm there. You’ll also find Lasm on npm. Search for @lasm/cli. And yeah, you basically npm install this project. The only dependency is Node. It will fully take care of everything else in the Lean toolchain, and the Clang, and LLVM, and Emscripten, and Binaryen, and all the crazy stuff that gets the Lean C code to compile into Wasm.

[24:35] It’s just all done for you behind the scenes. And I’ve been testing it out just a little bit manually or personally, you know, with a little Claude Code CLI help. And I mean, so far, it works. And you can see there’s a crazy test suite that, you know, you can go check out for yourself in the repo too. And you can try this out yourself as well. But yeah, I booted up an actual HTTP server in Lean running in Node on my computer, and I was able to curl into it, which is crazy. And yeah, go check out the project. There’s all kinds of benchmarks. I think we have things for like the cold starts, memory, requests per second, binary size, things like that.

[25:22] And, you know, I will be continuing to hone this project, plan to add all kinds of different testing methodologies, including working towards formal verification of Lasm itself. And then, yeah, the point is now the idea is, and this is it’s still a new project, right? It just launched, but open issues if there are problems. And, you know, I’m going to continue to use this and hopefully begin to adopt it, starting with their personal projects. And maybe if it makes sense professionally at the place that I work now. The idea is you can write your Cloudflare workers in Lean. Yeah, you could write your Express application now in Lean, your Hono app in Lean, and formally verify certain parts of those applications.

[26:20] The extent to which you can formally verify, I’m not super familiar with yet. You know, we have to think of the complexities of like, I don’t know, all the asynchronous and concurrent and in Lean opaque code because you can call into JavaScript, etc. I’ll be exploring a ton of that to find out like the limits of this and then figuring out, you know, how do we how do we remove those limits? The limits of the formal verification, right? Like, for example, when you call into a JavaScript library, like when you call from Lean into Hono. Well, that barrier right there, you know, your formal verification stops, right? But, you know, your server functionality, I would say probably like your authentication code, your business rules, all that stuff, I believe you can pull out into pretty pure functions.

[27:06] And then, you know, your IO, your, you know, the actual HTTP handler code that’s doing the input output stuff, like I don’t think you can. You could you could verify that to some extent, I believe, but all the business rules and the authentication and authorization, etc. Hopefully, the idea is you can write propositions for those and then prove them. And then on the front end, I haven’t even really touched front end yet, but like. The AI has told me it’s it’s right now it’s like an Elm like architecture, if you’re familiar with Elm for the front end and. Yeah, we’ll see. We’ll see. We’ll see. I’m super excited now. Lean is open for business in many more platforms where it was would have been very difficult to do before.

[27:56] And I encourage you to try it out. You just need Node, just Node and npm on your machine and you can get going. I probably recommend using VS Code and the Lean 4 extension. If you want to kind of dive into proof checking and stuff on your own or I mean, just go for it fully. You could call vibe coding if you want, but. I call it agentic engineering, if you are probing the AI, you know, asking it clarifying questions. If when you’re doing the formal verification, what you should do probably is really discuss the propositions that Lean has created.

[28:42] Learning the syntax is probably a good idea so you can understand the propositions natively, but also I’m not sure it’s strictly necessary. You can ask it like, all right, list out the propositions here and in plain English, let’s go over them. And, you know, you could have it triple check, bump the reasoning up to make sure that the intended behavior is characterized appropriately with each proposition being individually necessary and collectively sufficient to characterize the functionality of what you’re doing. Yeah, join me on this journey. Start learning Lean, start using Lasm and let’s begin to formally verify all software.

Support MillillionPodcast RSS