11 ms·

Lean proved this program correct; then I found a bug

395 points by bumbledraven 5mo ago

porcoda 5mo ago
I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does something other than what you intended. This is one of the harder parts of verification: clearly expressing your intention as a human. As programs get more complex these get harder to write, which means it isn’t uncommon to have lean or rocq proofs for everything only to later find “nope, it has a bug that ultimately traces back to a subtle specification defect.” Once you’ve gone through this a few times you quickly realize that tools like lean and rocq are tricky to use effectively. I kinda worry that the “proof assistants will fix ai correctness” will lead to a false sense of assurance if the specs that capture human intention don’t get scrutinized closely. Otherwise we’ll likely have lots of proofs for code that isn’t the code the humans actually intended due to spec flaws.
- jmalicki 5mo ago
  I have experience with similar things! But that's not saying the proofs are an issue - usually the spec you can reasonably prove in lean or another prover, say TLA+ or Z3 depending on your kind of program - has to be overly simplified and have a lot of assumptions. However, that is powerful. It doesn't mean your program doesn't have bugs. It means this big scary complicated algorithm you think works but are skeptical doesn't have bugs - so when you encounter one, you know the bug is elsewhere, and you start really looking at the boundaries of what could be misspecified, if the assumptions given to the prover are actually true, etc. It eliminates the big scary thing everyone will think is the cause of the bug as the actual cause. This has been insanely valuable to me lately. It is also something I never really was able to do before the help of AI - vibe coding proofs about my programs is IMO one of the killer apps of AI, since there aren't a ton of great resources yet about how to do it well since it is rarely done.
  - Nevermark 5mo ago
    That is damn insightful.
  - cubefox 5mo ago
    > This has been insanely valuable to me lately. This surprises me. Formal verification so far has been a very niche thing apart from conventional type systems. I didn't think lack of vibe coding was much of a bottleneck in the past. Where do you use it?
    - baq 5mo ago
      The problem is implementing anything approximately twice is a hard sell… this is no longer true, though - TLA+ models are cheap now. You should be using them when writing any sort of distributed systems, which is basically everything nowadays.
    - jmalicki 5mo ago
      Roughly anything that, say, has the complexity of a leetcode medium level problem that isn't already an extremely well known algorithm. Any moderately complex thread safety thing with a few moving parts (e.g. there are multiple mutexes involved in various parts of the system, verify no deadlocks). The lack of vibe coding has been a bottleneck for literally everything before. When I see people say the hate vibe coding, I think "why do you hate formal verification? Because you could be spending your time on formal verification instead of removing "code smells" that don't hurt anything from vibe code."
- brookst 5mo ago
  Been thinking about this a lot recently. I think we need a way to verify the specs. A combo of formal logic and adversarial thinking (probably from LLMs) that will produce an exhaustive list of everything the program will do, and everything it won’t do, and everything that is underspecified. Still not quite sure what it looks like, but if you stipulate that program generation will be provable, it pushes the correctness challenge up to the spec (and once we solve that, it’ll be pushed up to the requirements…)
  - frumplestlatz 5mo ago
    What’s important is to prove useful, high-level properties derived from the specs. The specs of program behavior are just the price of admission.
    - brookst 5mo ago
      I agree. It’s kind of like secure boot, in reverse: the high level stuff has to be complete and correct enough that the next level down has a chance to be complete and correct.
- somat 5mo ago
  Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them? You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bugs then the other? Why can one program have bugs but the other can't? How do you prove that you are proving the right thing? It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system. Don't get me wrong, I think these are great systems doing great work. But I always feel there is something missing in the narrative. I think a more practical view is that a program is already a sort of proof. there is a something to be solved and the program provides a mechanism to prove it. but this proof may be and probably is incorrect, as bugs are fixed it gets more and more correct. A powerful but time consuming tool to try and force correctness is to build the machine twice using different mechanisms. Then mismatched output indicates something is wrong with one of them. and your job as an engineer is to figure out which one. This is what formal verification brings to the table. The second mechanism.
  - rdevilla 5mo ago
    > It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system. Surely you are talking about Godel incompleteness, not Heisenberg's uncertainty principle; in which case they're actually not the same system - the verification/proof language is more like a metalanguage taking the implementation language as its object. (Godel's observation for mathematics was just that for formal number systems of sufficient power, you can embed that metalanguage into the formal number system itself.)
  - CJefferson 5mo ago
    The chances of significant bugs in lean which lead to false answers to real problems are extremely small (this bug still just caused a crash, but is still bad). Many, many people try very hard to break Lean, and think about how proofs work, and fail. Is it foolproof? No. It might have flaws, it might be logic itself is inconsistent. I often think of the ‘news level’ of a bug. A bug in most code wouldn’t be news. A bug which caused lean to claim a real proof someone cared about was true, when it wasn’t, would in the proof community the biggest news in a decade.
- andai 5mo ago
  Let me try wrap my head around this. I notice two classes of bugs in my own programs: - I meant the code to do X, but it does Y - I meant the code to do X, and it does X, but X causes problems I didn't foresee A proof assistant can help you prove the code does X, but it can't help you prove doing X doesn't cause problems you didn't foresee. In other words, it can prove the soundness of the implementation, but not the design? Is that right? Though I imagine if there are internal contradictions in the design, lean would catch those too. So the issue would be "internally consistent yet incorrect designs"? In the case of TFA, the issue was exhaustiveness, right? "What happens if..." That sounds like a pretty important quality as far as security goes. Is there a way to make sure everything is actually verified? I heard actually verifying everything is prohibitively expensive though, like it took 10-20 years to verify seL4 (10K LoC).
davesque 5mo ago
Am I reading the article wrong? It appears that the author did not test the claims of the proof. Wouldn't a "bug" in this case mean she found an input that did not survive a round trip through the compression algorithm? Update: Actually, I guess this may have been her point: "The two bugs that were found both sat outside the boundary of what the proofs cover." So then I guess the title might be a bit click baity.
- gopiandcode 5mo ago
  Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs. Secondly, I did find a bug in the algorithm. in Archive.lean, in the parsing of the compressed archive headers. That was the crashing input.
  - quantummagic 5mo ago
    > I think it's fair to consider the entire binary a fair target. Yes, it's still very much a bug. But it has nothing to do with your program being formally verified or not. Formal verification can do nothing about any unverified code you rely on. You would really need a formal verification of every piece of hardware, the operating system, the runtime, and your application code. Short of that, nobody should expect formal verification to ensure there are no bugs.
    - appplication 5mo ago
      I read it as that’s also the point. Adding formal verification is not a strict defense against bugs. It is in a way similar to having 100% test coverage and finding bugs in your untested edge cases. I don’t think the author is attempting to decry formal verification, but I think it a good message in the article everyone should keep in mind that safety is a larger, whole system process and bugs live in the cracks and interfaces.
lmm 5mo ago
Not verifying the parser seems like a pretty big oversight. Parsing binary formats is notoriously dangerous!
ctmnt 5mo ago
This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. Still an interesting and useful result to find a bug in the Lean runtime, but I’d argue that doesn’t justify the title. Or the claim that “the entire proof edifice” is somehow shaky. It’s important to note that this is the Lean runtime that has a bug, not the Lean kernel, which is the part that actually does the verification (aka proving). [1] So it’s not even immediately clear what this bug would really apply to, since obviously no one’s running any compiled Lean code in any kind of production hot path. [1] https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/ https://lean-lang.org/doc/reference/latest/Elaboration-and-C...
- gopiandcode 5mo ago
  Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs. Second, there was a bug in the code. Maybe not a functional correctness bug, but I, along with many and most end users, would consider a crashing program buggy. Maybe we just have different tastes or different standards on what we consider an acceptable level of software quality. W.r.t people running Lean in production, you'd be surprised...
  - danparsonson 5mo ago
    We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compelling statement, for the reasons you describe).
spullara 5mo ago
claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."
- germandiago 5mo ago
  Maybe we do not know what Claude has been doing and he keeps it secret...? :D
- gwern 5mo ago
  It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?
  - deleted 5mo ago
    [deleted]
  - spullara 5mo ago
    Meaning it has no episodic memory of any of those analyses that it has done.
    - gwern 5mo ago
      You didn't say anything about 'episodic' and that's irrelevant to the point even if its long-term memory from training didn't count.
dchftcs 5mo ago
This is analogous to the fundamental problem of better automation in programming - eventually, the complexity and correctness of of the spec takes over, and if we don't manage that well, creating the spec is not that much less work than the programming part. If your program was for the wrong thing, a proof of it is also wrong.
- butvacuum 5mo ago
  everybody also ignores that even hello world isn't deterministic anymore. It just doesn't matter to execution if something broke unless it kicks back an error. although, this is the best example of how quickly a trivality can knock so called "correct" programs over.
- jongjong 5mo ago
  Fully agree. I started hitting this bottleneck when I combined a low-code backend I built with Claude Code to generate web applications. I can build applications rapidly but the requirements and UX are the bottleneck. So much so that I often like to sit on a concept for multiple days to give myself the time to fully absorb the goal and refine the requirements. Then once I know what to build, it snaps together in like 4 hours. There are a lot of ambiguities which need to be resolved ahead of time. Software engineering becomes a kind of detailed business strategy role.
  - Paracompact 5mo ago
    I'm curious about your learning experience, but what was the nature of your bottleneck, exactly? Was the backend perfectly fine as a backend, but Claude struggled to wire it to a frontend gracefully?
    - jongjong 5mo ago
      Claude does a great job generating the code. The hard part was the UX like if the app gets complex, then I want a new feature which adds more complexity on top; because of the way the application/UX is designed, it's hard to integrate that feature in a way that's not confusing to the user. Like for example, I used check boxes to mean "include the records in the result set" but in a different section later in the flow, I have a different but similar looking view/list of records but I just want to use the check boxes to do batch delete but don't want the user to think that this means "include in the result set" in this case. So maybe instead I need a different single checkbox at the top which says "Don't ask for confirmation" so the user can just click on the normal "delete icon" on each row to delete the entries quickly without being prompted... But on the other previous view/list I allow the user to use the check boxes to both include the record but also batch delete using a single small cross at the top... But in the later section I mentioned, I don't want to do this because of the way I designed the flow, it would confuse the user and make it hard for them to track what they're doing and where they made the change (I want the selection step to be in a single place, the current page serves a different purpose). So maybe I need to change the other page as well for consistency... And use the "Don't ask for delete confirmation" approach everywhere? But there's not enough space to fit that text on those other pages... When you solve all the hard problems, this is what coding gets reduced to. Not a hard problem but it's like lots of small ones like that which keep coming up and your interface ends up with a complex URL scheme and lot of modals and nested tabs.
mindcrime 5mo ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth
ernsheong 5mo ago
Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct. [1] https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem
- lmm 5mo ago
  And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.
  - AnimalMuppet 5mo ago
    Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).
    - gopiandcode 5mo ago
      you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/ https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/ https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
      - DonaldPShimoda 5mo ago
        > finite programs that run on an infinite stream of events This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
san_tekart 5mo ago
[flagged]
jongjong 5mo ago
Formal proofs can only ever work to validate against requirements... But a major issue with a lot of modern software is that the requirements themselves can be incorrect and some requirements can logically conflict with other requirements... So long as we have non-technical people formulating requirements, we can never have provably correct software. I've come across issues in the past which weren't actually bugs. For example, the software was behaving exactly as intended but it looked like a bug to a user who didn't understand the nuances and complexities of what was happening. I also cannot count how many times a non-technical person asked me to implement conflicting functionality or functionality which would have made the UX incredibly confusing for the user.
grg0 5mo ago
Clickbait title, the proved part of the program had no bugs? As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.
- nickvec 5mo ago
  Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.
  - grg0 5mo ago
    And it took them several thousand words to explain what you just said in a sentence.
    - nickvec 5mo ago
      Definitely one of my biggest pet peeves with articles / blog posts. There is so much fluff. Just get to the point!
  - minimaltom 5mo ago
    The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug). Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.
    - deleted 5mo ago
      [deleted]
- minimaltom 5mo ago
  Is it fair when it comes to formally-verified software to only consider bugs that violate a proof, and ignore everything else? Formally-verified software is usually advertised "look ma no bugs!" Not "look ma no bugs*" *As long as this complicated chain of lemmas appropriately represents the correctness of everything we care about. In boating theres often debate of right of way rules in certain situations, and some people are quick to point out that giant tanker ships should be giving way to tiny sailboats and get all worked up about it*. The best answer I've heard: they're dead right! that is to say as right as they are dead (if they didnt yield) lol. In the same vein, I think someone who assumed that a formally-verified software was perfect and got hacked or whatever is going to be a bit wiggly about the whole thing. * = Technically the rules prioritize the tankers if they are "restricted in ability to maneuver" but everyone loves to argue about that.
youknownothing 5mo ago
I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you didn't make a mistake in your formal verification? IOW, how do you know your formal verification is bug-free? Answer: you don't. Or if you try to formally verify your formal verification then you're just translating the problem to a new layer. It's just a chain of proofs that is always ultimately based on an unproven one, which invalidates the whole chain. You can get asymptotically close to zero-bug proof, but you can never get there 100% of the way.
- zitterbewegung 5mo ago
  The better look at this is not to prove that you have no bugs is that to prove that a program conforms to a specification that Lean can verify. Even with the addition of two numbers the execution of a program can be wrong if the CPU has a fault or if the runtime of the program has a bug. I think you just need to look at why formal verification exists.
- aaronblohowiak 5mo ago
  I disagree but the constraints required to get there are probably untenable for most practical applications, so in practice I agree.
- thatguysaguy 5mo ago
  What is up with people saying you cannot prove a negative? Of course you can! (At least in formal settings) For example it's extremely easy to prove there is no square with diagonals of different lengths. I'm the hard end, Andrew Wiles proved Fermat's Last Theorem which expresses a negative. That's just a nit though, you're right about the infinite regress problem.
  - pxc 5mo ago
    It's pretty easy to prove lots of negatives outside of mathematics, too. It's easy to prove there's no elephant in my living room at the moment.
readthenotes1 5mo ago
I didn't like the clickbait title. I would have preferred something along the lines of "Lean proves other program correct but not itself"
vatsachak 5mo ago
You guys are missing the forest for the trees. They used an AI agent sending ideas to a fuzzer and discovered a heap buffer overflow in Lean. This is big.
- germandiago 5mo ago
  Indeed this is a nice discovery and I think it is useful in its own right.
akoboldfrying 5mo ago
Nice work. Amusing that Lean's own standard library has a buffer overflow bug, which "leaked out" due to being exempted from the verification. Regarding the DoS in the lean-zip application itself: I think this is a really neat example of the difficult problem of spec completeness, which is a subcase of the general problem (mentioned by porcoda in a sibling comment) of being sure that the spec is checking the right things. For a compression program, the natural, and I would also say satisfyingly beautiful thing to prove is that decomp(comp(x)) = x for all possible inputs x. It's tempting to think that at that point, "It's proven!" But of course the real world can call decomp() on something that has never been through comp() at all, and this simple, beautiful spec is completely silent on what will happen then.
ozten 5mo ago
HN to be renamed Flex Social. Damn.
sebstefan 5mo ago
So that's just one more win for formal verification despite the title it seems I'm genuinely excited about AI agents and formal verification languages. To me it's obviously the way forward instead of moonshots trying to make agents that program in their own AI blackbox binary, or agents that code in current programming languages. If we are heading in the direction of "huge codebases that nobody has written", or, "code is an artifact for the machine", I don't see a way out without making it proved. If humans can review and edit the spec, then verify that the implementation matches it, suddenly leaving the implementation be an artifact for the machines seems okay The downside of provers also being that they are a massive pain in the ass that very few want to use, this is also a complete win.
ajaystream 5mo ago
The spec-completeness problem here is the same one that bites distributed systems verification: the proof holds inside an operating envelope (no adversarial inputs, trusted runtime, bounded sizes), and the interesting failures live at the boundary. TLA+ has the same property - you can prove liveness under a fairness assumption the deployment silently violates, and nothing in the proof tells you when reality drifted outside. What I'd actually want from the tooling is a machine-checkable statement of the envelope itself, propagated as a runtime guard rather than a compile-time comment. Then "proof holds" and "we are still inside the proof's domain" are two separate, observable properties, and the unverified-parser / unverified-runtime cases stop being invisible.
- aidenn0 5mo ago
  As someone who has discovered a bug in a CPU that was previously unknown to our chip vendor, I would like to point out that the rabbit hole is deep. On the other hand, I've discovered thousands of bugs that weren't hardware bugs, and dozens of bugs due to people not having read hardware errata documents, so just formally modeling what we can model will absurdly reduce the bug quantity.
  - ajaystream 5mo ago
    [dead]
Animats 5mo ago
Compression/decompression is a good problem for proof of correctness. The specification is very simple (you must get back what you put in), while the implementation is complex. What seems to have happened here is that the storage allocator underneath is unverified. That, too, has a relatively simple spec - all buffers disjoint, no lost buffers, no crashes.
sammy2255 5mo ago
[flagged]
- operatingthetan 5mo ago
  Are you sensitive to colors?
  - sammy2255 5mo ago
    [flagged]
    - deleted 5mo ago
      [deleted]
raverbashing 5mo ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth https://news.ycombinator.com/item?id=12761986 https://news.ycombinator.com/item?id=12761986 (being this link more than 10yrs old is not surprising)
ButlerianJihad 5mo ago
Incorrect usage of semicolon in title/headline. Should be a comma. Tsk, tsk.
rhdunn 5mo ago
Tools like this (formal verification, sparse, etc.) and built-in mechanism (types, generics, RAII, rust's borrow checker) can only verify issues within the scope of that framework. There are also trade-offs and limitations with each type and each implementation. Type checking allows you to (outside of type casting such as in languages like C/C++ and casting to object for generic containers in Java) verify that an object is of a given type. That allows you to be sure that a well-formed program isn't doing things like putting a random object in a list. Languages like C#, Scala, and Kotlin improve Java generics by making the generic type of a container or other interface/type part of the type system. This allows generic types of a generic type to preserve the inner type. This makes it possible to implement things like monads and mapping functions to preserve the generic type. A similar thing is possible with union types, sealed interfaces/traits, etc. that allow you to check and verify the return type instead of defaulting it to a generic object/any type. Likewise with other features like nullable/non-null annotations (or corresponding nullable type annotations like in Kotlin and recent C# versions). All of these can be abused/circumvented, but if you keep your code within that framework the compiler will stop that code compiling. Likewise, these solve a limited set of bugs. For example, nullable types can't verify memory management and related bugs.
seanhunter 5mo ago
This is very cool work but the author is labouring under a false premise about how axiomatic systems work: > Every Lean proof assumes the runtime is correct. No. Every valid Lean proof assumes that if the runtime/mathlib etc is correct, then it too is correct. Tangentially also, most lean proofs are not dependent on whether or not the runtime has things like buffer overflows or denial of service against lean itself at all, because if I prove some result in Lean (without attacking the runtime) then a bug in the runtime doesn’t affect the validity of the result in general. It does mean however that it’s not ok to blindly trust a proof just because it only relies on standard axioms and has no “sorry”s. You also need to check that the proof doesn’t exploit lean itself.
crvdgc 5mo ago
Unfortunately, the discussion focused on the somewhat click baity title "proved this program correct". It's unclear what "this program" is. If it refers to the core algorithm with a proof, then there's no bug. If it includes the runtime and the header parser, then Lean didn't prove it correct. That being said, using a coding agent to direct fuzzying and find bugs in the Lean kernel implementation is the big news here. (After all the kernel's implementation is not proved.) The moral of the story is to push for more verified code not less and try AI bug hunting.
sylware 5mo ago
c++, you asked for it.
aesopturtle 5mo ago
This is a great reminder that ‘proved correct’ always has an invisible suffix: ‘with respect to the thing you actually specified.’ The hard part was never just proving things, it was pinning reality down tightly enough that the proof is about the right world.
vfclists 5mo ago
Correctness with respect to a specification is not the same as correctness with respect to intent(ion) or expectation
DoctorOetker 5mo ago
So this is very good news and was predictable. LLM's are capable of producing code that passes formal verification. The writing is on the wall: in the future more and more software on the abstract or platonic side of our computing base will be hermetically sealed against bugs and exploits. This quenching of bugs in the assured side will shift the mean location of bugs closer to the hardware side: at some point bugs and exploits will rely more and more on hardware quirks, and simply unspecified hardware. Afterwards we can expect a long exponential decay of preventable safety violations: people mistakenly or surreptitiously disengaging the formal verification steps and shipping malicious or unverified code. Each such event will be its own big or small scandal, at some point there will be no deniability left: something must be on purpouse, either a malicious vulnerability or intentional disengagement of safety measures. As the attack surface recedes towards the lower level hardware stack, it will open the debate that the community needs proper formal hardware descriptions (at least at the interface initially, not necessarily how the hardware has implemented it). As interface bugs get formalized 3 things can happen: either vulnerabilities go extinct, and full formal hardware descriptions are not released or vulnerabilities remain in each new generation of hardware, and malicious intent or negligence on behalf of the manufacturer can only be presumed, this will set up the community against manufacturers, as they demand full hardware descriptions (verilog, VHDL,...). or vulnerabilities are tactically applied (vulnerabilities appear extinct to the bulk of the population, but only because manufactured vulnerabilities are sparingly exploited by the manufacturing block) It is hard to predict what is more valuable: embedding HW vulnerabilities for the status quo and being able to exploit it for while before the public demands full hardware IP descriptions (verilog, VHDL) etc. or facing the end of vulnerabilities a little sooner but keeping hardware IP private (if the bugs stop with full interface descriptions).
Alifatisk 5mo ago
> The two bugs that were found both sat outside the boundary of what the proofs cover Are we baiting people with headlines now?
vvern 5mo ago
Now I want to see benchmarks
justinclift 5mo ago
> 105,823,818 fuzzing executions. That sounds like quite the monthly bill. o_O
deterministic 5mo ago
"The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct (and now has a PR addressing)." In other words, the code was proven correct according to spec by LEAN. Which is exactly what LEAN claims to do.

395 points by bumbledraven 5mo ago

I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does something other than what you intended. This is one of the harder parts of verification: clearly expressing your intention as a human. As programs get more complex these get harder to write, which means it isn’t uncommon to have lean or rocq proofs for everything only to later find “nope, it has a bug that ultimately traces back to a subtle specification defect.” Once you’ve gone through this a few times you quickly realize that tools like lean and rocq are tricky to use effectively. I kinda worry that the “proof assistants will fix ai correctness” will lead to a false sense of assurance if the specs that capture human intention don’t get scrutinized closely. Otherwise we’ll likely have lots of proofs for code that isn’t the code the humans actually intended due to spec flaws.

jmalicki 5mo ago
I have experience with similar things! But that's not saying the proofs are an issue - usually the spec you can reasonably prove in lean or another prover, say TLA+ or Z3 depending on your kind of program - has to be overly simplified and have a lot of assumptions. However, that is powerful. It doesn't mean your program doesn't have bugs. It means this big scary complicated algorithm you think works but are skeptical doesn't have bugs - so when you encounter one, you know the bug is elsewhere, and you start really looking at the boundaries of what could be misspecified, if the assumptions given to the prover are actually true, etc. It eliminates the big scary thing everyone will think is the cause of the bug as the actual cause. This has been insanely valuable to me lately. It is also something I never really was able to do before the help of AI - vibe coding proofs about my programs is IMO one of the killer apps of AI, since there aren't a ton of great resources yet about how to do it well since it is rarely done.
- Nevermark 5mo ago
  That is damn insightful.
- cubefox 5mo ago
  > This has been insanely valuable to me lately. This surprises me. Formal verification so far has been a very niche thing apart from conventional type systems. I didn't think lack of vibe coding was much of a bottleneck in the past. Where do you use it?
  - baq 5mo ago
    The problem is implementing anything approximately twice is a hard sell… this is no longer true, though - TLA+ models are cheap now. You should be using them when writing any sort of distributed systems, which is basically everything nowadays.
  - jmalicki 5mo ago
    Roughly anything that, say, has the complexity of a leetcode medium level problem that isn't already an extremely well known algorithm. Any moderately complex thread safety thing with a few moving parts (e.g. there are multiple mutexes involved in various parts of the system, verify no deadlocks). The lack of vibe coding has been a bottleneck for literally everything before. When I see people say the hate vibe coding, I think "why do you hate formal verification? Because you could be spending your time on formal verification instead of removing "code smells" that don't hurt anything from vibe code."
brookst 5mo ago
Been thinking about this a lot recently. I think we need a way to verify the specs. A combo of formal logic and adversarial thinking (probably from LLMs) that will produce an exhaustive list of everything the program will do, and everything it won’t do, and everything that is underspecified. Still not quite sure what it looks like, but if you stipulate that program generation will be provable, it pushes the correctness challenge up to the spec (and once we solve that, it’ll be pushed up to the requirements…)
- frumplestlatz 5mo ago
  What’s important is to prove useful, high-level properties derived from the specs. The specs of program behavior are just the price of admission.
  - brookst 5mo ago
    I agree. It’s kind of like secure boot, in reverse: the high level stuff has to be complete and correct enough that the next level down has a chance to be complete and correct.
somat 5mo ago
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them? You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bugs then the other? Why can one program have bugs but the other can't? How do you prove that you are proving the right thing? It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system. Don't get me wrong, I think these are great systems doing great work. But I always feel there is something missing in the narrative. I think a more practical view is that a program is already a sort of proof. there is a something to be solved and the program provides a mechanism to prove it. but this proof may be and probably is incorrect, as bugs are fixed it gets more and more correct. A powerful but time consuming tool to try and force correctness is to build the machine twice using different mechanisms. Then mismatched output indicates something is wrong with one of them. and your job as an engineer is to figure out which one. This is what formal verification brings to the table. The second mechanism.
- rdevilla 5mo ago
  > It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system. Surely you are talking about Godel incompleteness, not Heisenberg's uncertainty principle; in which case they're actually not the same system - the verification/proof language is more like a metalanguage taking the implementation language as its object. (Godel's observation for mathematics was just that for formal number systems of sufficient power, you can embed that metalanguage into the formal number system itself.)
- CJefferson 5mo ago
  The chances of significant bugs in lean which lead to false answers to real problems are extremely small (this bug still just caused a crash, but is still bad). Many, many people try very hard to break Lean, and think about how proofs work, and fail. Is it foolproof? No. It might have flaws, it might be logic itself is inconsistent. I often think of the ‘news level’ of a bug. A bug in most code wouldn’t be news. A bug which caused lean to claim a real proof someone cared about was true, when it wasn’t, would in the proof community the biggest news in a decade.
andai 5mo ago
Let me try wrap my head around this. I notice two classes of bugs in my own programs: - I meant the code to do X, but it does Y - I meant the code to do X, and it does X, but X causes problems I didn't foresee A proof assistant can help you prove the code does X, but it can't help you prove doing X doesn't cause problems you didn't foresee. In other words, it can prove the soundness of the implementation, but not the design? Is that right? Though I imagine if there are internal contradictions in the design, lean would catch those too. So the issue would be "internally consistent yet incorrect designs"? In the case of TFA, the issue was exhaustiveness, right? "What happens if..." That sounds like a pretty important quality as far as security goes. Is there a way to make sure everything is actually verified? I heard actually verifying everything is prohibitively expensive though, like it took 10-20 years to verify seL4 (10K LoC).

davesque 5mo ago

Am I reading the article wrong? It appears that the author did not test the claims of the proof. Wouldn't a "bug" in this case mean she found an input that did not survive a round trip through the compression algorithm? Update: Actually, I guess this may have been her point: "The two bugs that were found both sat outside the boundary of what the proofs cover." So then I guess the title might be a bit click baity.

gopiandcode 5mo ago
Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs. Secondly, I did find a bug in the algorithm. in Archive.lean, in the parsing of the compressed archive headers. That was the crashing input.
- quantummagic 5mo ago
  > I think it's fair to consider the entire binary a fair target. Yes, it's still very much a bug. But it has nothing to do with your program being formally verified or not. Formal verification can do nothing about any unverified code you rely on. You would really need a formal verification of every piece of hardware, the operating system, the runtime, and your application code. Short of that, nobody should expect formal verification to ensure there are no bugs.
  - appplication 5mo ago
    I read it as that’s also the point. Adding formal verification is not a strict defense against bugs. It is in a way similar to having 100% test coverage and finding bugs in your untested edge cases. I don’t think the author is attempting to decry formal verification, but I think it a good message in the article everyone should keep in mind that safety is a larger, whole system process and bugs live in the cracks and interfaces.

lmm 5mo ago

Not verifying the parser seems like a pretty big oversight. Parsing binary formats is notoriously dangerous!

ctmnt 5mo ago

This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. Still an interesting and useful result to find a bug in the Lean runtime, but I’d argue that doesn’t justify the title. Or the claim that “the entire proof edifice” is somehow shaky. It’s important to note that this is the Lean runtime that has a bug, not the Lean kernel, which is the part that actually does the verification (aka proving). [1] So it’s not even immediately clear what this bug would really apply to, since obviously no one’s running any compiled Lean code in any kind of production hot path. [1] https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/ https://lean-lang.org/doc/reference/latest/Elaboration-and-C...

gopiandcode 5mo ago
Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs. Second, there was a bug in the code. Maybe not a functional correctness bug, but I, along with many and most end users, would consider a crashing program buggy. Maybe we just have different tastes or different standards on what we consider an acceptable level of software quality. W.r.t people running Lean in production, you'd be surprised...
- danparsonson 5mo ago
  We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compelling statement, for the reasons you describe).

spullara 5mo ago

claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."

germandiago 5mo ago
Maybe we do not know what Claude has been doing and he keeps it secret...? :D
gwern 5mo ago
It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?
- deleted 5mo ago
  [deleted]
- spullara 5mo ago
  Meaning it has no episodic memory of any of those analyses that it has done.
  - gwern 5mo ago
    You didn't say anything about 'episodic' and that's irrelevant to the point even if its long-term memory from training didn't count.

dchftcs 5mo ago

This is analogous to the fundamental problem of better automation in programming - eventually, the complexity and correctness of of the spec takes over, and if we don't manage that well, creating the spec is not that much less work than the programming part. If your program was for the wrong thing, a proof of it is also wrong.

butvacuum 5mo ago
everybody also ignores that even hello world isn't deterministic anymore. It just doesn't matter to execution if something broke unless it kicks back an error. although, this is the best example of how quickly a trivality can knock so called "correct" programs over.
jongjong 5mo ago
Fully agree. I started hitting this bottleneck when I combined a low-code backend I built with Claude Code to generate web applications. I can build applications rapidly but the requirements and UX are the bottleneck. So much so that I often like to sit on a concept for multiple days to give myself the time to fully absorb the goal and refine the requirements. Then once I know what to build, it snaps together in like 4 hours. There are a lot of ambiguities which need to be resolved ahead of time. Software engineering becomes a kind of detailed business strategy role.
- Paracompact 5mo ago
  I'm curious about your learning experience, but what was the nature of your bottleneck, exactly? Was the backend perfectly fine as a backend, but Claude struggled to wire it to a frontend gracefully?
  - jongjong 5mo ago
    Claude does a great job generating the code. The hard part was the UX like if the app gets complex, then I want a new feature which adds more complexity on top; because of the way the application/UX is designed, it's hard to integrate that feature in a way that's not confusing to the user. Like for example, I used check boxes to mean "include the records in the result set" but in a different section later in the flow, I have a different but similar looking view/list of records but I just want to use the check boxes to do batch delete but don't want the user to think that this means "include in the result set" in this case. So maybe instead I need a different single checkbox at the top which says "Don't ask for confirmation" so the user can just click on the normal "delete icon" on each row to delete the entries quickly without being prompted... But on the other previous view/list I allow the user to use the check boxes to both include the record but also batch delete using a single small cross at the top... But in the later section I mentioned, I don't want to do this because of the way I designed the flow, it would confuse the user and make it hard for them to track what they're doing and where they made the change (I want the selection step to be in a single place, the current page serves a different purpose). So maybe I need to change the other page as well for consistency... And use the "Don't ask for delete confirmation" approach everywhere? But there's not enough space to fit that text on those other pages... When you solve all the hard problems, this is what coding gets reduced to. Not a hard problem but it's like lots of small ones like that which keep coming up and your interface ends up with a complex URL scheme and lot of modals and nested tabs.

mindcrime 5mo ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." -- Donald Knuth

ernsheong 5mo ago

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct. [1] https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem

lmm 5mo ago
And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.
- AnimalMuppet 5mo ago
  Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).
  - gopiandcode 5mo ago
    you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/ https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/ https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
    - DonaldPShimoda 5mo ago
      > finite programs that run on an infinite stream of events This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.

san_tekart 5mo ago

[flagged]

jongjong 5mo ago

Formal proofs can only ever work to validate against requirements... But a major issue with a lot of modern software is that the requirements themselves can be incorrect and some requirements can logically conflict with other requirements... So long as we have non-technical people formulating requirements, we can never have provably correct software. I've come across issues in the past which weren't actually bugs. For example, the software was behaving exactly as intended but it looked like a bug to a user who didn't understand the nuances and complexities of what was happening. I also cannot count how many times a non-technical person asked me to implement conflicting functionality or functionality which would have made the UX incredibly confusing for the user.

grg0 5mo ago

Clickbait title, the proved part of the program had no bugs? As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.

nickvec 5mo ago
Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.
- grg0 5mo ago
  And it took them several thousand words to explain what you just said in a sentence.
  - nickvec 5mo ago
    Definitely one of my biggest pet peeves with articles / blog posts. There is so much fluff. Just get to the point!
- minimaltom 5mo ago
  The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug). Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.
  - deleted 5mo ago
    [deleted]
minimaltom 5mo ago
Is it fair when it comes to formally-verified software to only consider bugs that violate a proof, and ignore everything else? Formally-verified software is usually advertised "look ma no bugs!" Not "look ma no bugs*" *As long as this complicated chain of lemmas appropriately represents the correctness of everything we care about. In boating theres often debate of right of way rules in certain situations, and some people are quick to point out that giant tanker ships should be giving way to tiny sailboats and get all worked up about it*. The best answer I've heard: they're dead right! that is to say as right as they are dead (if they didnt yield) lol. In the same vein, I think someone who assumed that a formally-verified software was perfect and got hacked or whatever is going to be a bit wiggly about the whole thing. * = Technically the rules prioritize the tankers if they are "restricted in ability to maneuver" but everyone loves to argue about that.

youknownothing 5mo ago

I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you didn't make a mistake in your formal verification? IOW, how do you know your formal verification is bug-free? Answer: you don't. Or if you try to formally verify your formal verification then you're just translating the problem to a new layer. It's just a chain of proofs that is always ultimately based on an unproven one, which invalidates the whole chain. You can get asymptotically close to zero-bug proof, but you can never get there 100% of the way.

zitterbewegung 5mo ago
The better look at this is not to prove that you have no bugs is that to prove that a program conforms to a specification that Lean can verify. Even with the addition of two numbers the execution of a program can be wrong if the CPU has a fault or if the runtime of the program has a bug. I think you just need to look at why formal verification exists.
aaronblohowiak 5mo ago
I disagree but the constraints required to get there are probably untenable for most practical applications, so in practice I agree.
thatguysaguy 5mo ago
What is up with people saying you cannot prove a negative? Of course you can! (At least in formal settings) For example it's extremely easy to prove there is no square with diagonals of different lengths. I'm the hard end, Andrew Wiles proved Fermat's Last Theorem which expresses a negative. That's just a nit though, you're right about the infinite regress problem.
- pxc 5mo ago
  It's pretty easy to prove lots of negatives outside of mathematics, too. It's easy to prove there's no elephant in my living room at the moment.

readthenotes1 5mo ago

I didn't like the clickbait title. I would have preferred something along the lines of "Lean proves other program correct but not itself"

vatsachak 5mo ago

You guys are missing the forest for the trees. They used an AI agent sending ideas to a fuzzer and discovered a heap buffer overflow in Lean. This is big.

germandiago 5mo ago
Indeed this is a nice discovery and I think it is useful in its own right.

akoboldfrying 5mo ago

Nice work. Amusing that Lean's own standard library has a buffer overflow bug, which "leaked out" due to being exempted from the verification. Regarding the DoS in the lean-zip application itself: I think this is a really neat example of the difficult problem of spec completeness, which is a subcase of the general problem (mentioned by porcoda in a sibling comment) of being sure that the spec is checking the right things. For a compression program, the natural, and I would also say satisfyingly beautiful thing to prove is that decomp(comp(x)) = x for all possible inputs x. It's tempting to think that at that point, "It's proven!" But of course the real world can call decomp() on something that has never been through comp() at all, and this simple, beautiful spec is completely silent on what will happen then.

ozten 5mo ago

HN to be renamed Flex Social. Damn.

sebstefan 5mo ago

So that's just one more win for formal verification despite the title it seems I'm genuinely excited about AI agents and formal verification languages. To me it's obviously the way forward instead of moonshots trying to make agents that program in their own AI blackbox binary, or agents that code in current programming languages. If we are heading in the direction of "huge codebases that nobody has written", or, "code is an artifact for the machine", I don't see a way out without making it proved. If humans can review and edit the spec, then verify that the implementation matches it, suddenly leaving the implementation be an artifact for the machines seems okay The downside of provers also being that they are a massive pain in the ass that very few want to use, this is also a complete win.

ajaystream 5mo ago

The spec-completeness problem here is the same one that bites distributed systems verification: the proof holds inside an operating envelope (no adversarial inputs, trusted runtime, bounded sizes), and the interesting failures live at the boundary. TLA+ has the same property - you can prove liveness under a fairness assumption the deployment silently violates, and nothing in the proof tells you when reality drifted outside. What I'd actually want from the tooling is a machine-checkable statement of the envelope itself, propagated as a runtime guard rather than a compile-time comment. Then "proof holds" and "we are still inside the proof's domain" are two separate, observable properties, and the unverified-parser / unverified-runtime cases stop being invisible.

aidenn0 5mo ago
As someone who has discovered a bug in a CPU that was previously unknown to our chip vendor, I would like to point out that the rabbit hole is deep. On the other hand, I've discovered thousands of bugs that weren't hardware bugs, and dozens of bugs due to people not having read hardware errata documents, so just formally modeling what we can model will absurdly reduce the bug quantity.
- ajaystream 5mo ago
  [dead]

Animats 5mo ago

Compression/decompression is a good problem for proof of correctness. The specification is very simple (you must get back what you put in), while the implementation is complex. What seems to have happened here is that the storage allocator underneath is unverified. That, too, has a relatively simple spec - all buffers disjoint, no lost buffers, no crashes.

sammy2255 5mo ago

[flagged]

operatingthetan 5mo ago
Are you sensitive to colors?
- sammy2255 5mo ago
  [flagged]
  - deleted 5mo ago
    [deleted]

raverbashing 5mo ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth https://news.ycombinator.com/item?id=12761986 https://news.ycombinator.com/item?id=12761986 (being this link more than 10yrs old is not surprising)

ButlerianJihad 5mo ago

Incorrect usage of semicolon in title/headline. Should be a comma. Tsk, tsk.

rhdunn 5mo ago

Tools like this (formal verification, sparse, etc.) and built-in mechanism (types, generics, RAII, rust's borrow checker) can only verify issues within the scope of that framework. There are also trade-offs and limitations with each type and each implementation. Type checking allows you to (outside of type casting such as in languages like C/C++ and casting to object for generic containers in Java) verify that an object is of a given type. That allows you to be sure that a well-formed program isn't doing things like putting a random object in a list. Languages like C#, Scala, and Kotlin improve Java generics by making the generic type of a container or other interface/type part of the type system. This allows generic types of a generic type to preserve the inner type. This makes it possible to implement things like monads and mapping functions to preserve the generic type. A similar thing is possible with union types, sealed interfaces/traits, etc. that allow you to check and verify the return type instead of defaulting it to a generic object/any type. Likewise with other features like nullable/non-null annotations (or corresponding nullable type annotations like in Kotlin and recent C# versions). All of these can be abused/circumvented, but if you keep your code within that framework the compiler will stop that code compiling. Likewise, these solve a limited set of bugs. For example, nullable types can't verify memory management and related bugs.

seanhunter 5mo ago

This is very cool work but the author is labouring under a false premise about how axiomatic systems work: > Every Lean proof assumes the runtime is correct. No. Every valid Lean proof assumes that if the runtime/mathlib etc is correct, then it too is correct. Tangentially also, most lean proofs are not dependent on whether or not the runtime has things like buffer overflows or denial of service against lean itself at all, because if I prove some result in Lean (without attacking the runtime) then a bug in the runtime doesn’t affect the validity of the result in general. It does mean however that it’s not ok to blindly trust a proof just because it only relies on standard axioms and has no “sorry”s. You also need to check that the proof doesn’t exploit lean itself.

crvdgc 5mo ago

Unfortunately, the discussion focused on the somewhat click baity title "proved this program correct". It's unclear what "this program" is. If it refers to the core algorithm with a proof, then there's no bug. If it includes the runtime and the header parser, then Lean didn't prove it correct. That being said, using a coding agent to direct fuzzying and find bugs in the Lean kernel implementation is the big news here. (After all the kernel's implementation is not proved.) The moral of the story is to push for more verified code not less and try AI bug hunting.

sylware 5mo ago

c++, you asked for it.

aesopturtle 5mo ago

This is a great reminder that ‘proved correct’ always has an invisible suffix: ‘with respect to the thing you actually specified.’ The hard part was never just proving things, it was pinning reality down tightly enough that the proof is about the right world.

vfclists 5mo ago

Correctness with respect to a specification is not the same as correctness with respect to intent(ion) or expectation

DoctorOetker 5mo ago

So this is very good news and was predictable. LLM's are capable of producing code that passes formal verification. The writing is on the wall: in the future more and more software on the abstract or platonic side of our computing base will be hermetically sealed against bugs and exploits. This quenching of bugs in the assured side will shift the mean location of bugs closer to the hardware side: at some point bugs and exploits will rely more and more on hardware quirks, and simply unspecified hardware. Afterwards we can expect a long exponential decay of preventable safety violations: people mistakenly or surreptitiously disengaging the formal verification steps and shipping malicious or unverified code. Each such event will be its own big or small scandal, at some point there will be no deniability left: something must be on purpouse, either a malicious vulnerability or intentional disengagement of safety measures. As the attack surface recedes towards the lower level hardware stack, it will open the debate that the community needs proper formal hardware descriptions (at least at the interface initially, not necessarily how the hardware has implemented it). As interface bugs get formalized 3 things can happen: either vulnerabilities go extinct, and full formal hardware descriptions are not released or vulnerabilities remain in each new generation of hardware, and malicious intent or negligence on behalf of the manufacturer can only be presumed, this will set up the community against manufacturers, as they demand full hardware descriptions (verilog, VHDL,...). or vulnerabilities are tactically applied (vulnerabilities appear extinct to the bulk of the population, but only because manufactured vulnerabilities are sparingly exploited by the manufacturing block) It is hard to predict what is more valuable: embedding HW vulnerabilities for the status quo and being able to exploit it for while before the public demands full hardware IP descriptions (verilog, VHDL) etc. or facing the end of vulnerabilities a little sooner but keeping hardware IP private (if the bugs stop with full interface descriptions).

Alifatisk 5mo ago

> The two bugs that were found both sat outside the boundary of what the proofs cover Are we baiting people with headlines now?

vvern 5mo ago

Now I want to see benchmarks

justinclift 5mo ago

> 105,823,818 fuzzing executions. That sounds like quite the monthly bill. o_O

deterministic 5mo ago

"The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct (and now has a PR addressing)." In other words, the code was proven correct according to spec by LEAN. Which is exactly what LEAN claims to do.