Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lean proved this program correct; then I found a bug

kirancodes.me

Post reply on HN
Print view View original

61–70 of 186 posts

Re: Lean proved this program correct; then I found a bug

#61

Post by grg0 »

minimaltom wrote: post #35
grg0 wrote: post #24

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.

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 pe…

Nobody with experience in the field advertises formally-verified software like that, and it is understood that the spec may as well be wrong. It is also understood that the non-verified parts may have bugs (surprise). There is no news here.

Re: Lean proved this program correct; then I found a bug

#63

Post by sebstefan »

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.

Re: Lean proved this program correct; then I found a bug

#64

Post by quantummagic »

appplication wrote: post #37
quantummagic wrote: post #12

Earlier quoted context omitted.

> 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 for…

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…

You're right. It just seems as though it should be self-evident. Especially to those sophisticated enough to understand and employ formal verification.

Re: Lean proved this program correct; then I found a bug

#65

Post by Nevermark »

jmalicki wrote: post #5
porcoda wrote: post #2

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…

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…

That is damn insightful.

Re: Lean proved this program correct; then I found a bug

#66

Post by danparsonson »

gopiandcode wrote: post #9
ctmnt wrote: post #6

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. St…

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.…

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).

Re: Lean proved this program correct; then I found a bug

#67

Post by Nevermark »

somat wrote: post #33
porcoda wrote: post #2

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…

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 bu…

A program is a hard proof of existence.

It runs (maybe crashes), therefore … it exists.

The tension between spec bugs vs. implementation bugs is real. But i will take a bug in a situation where the implementation has been verified any day.

Working over what we really want is problem solving in the problem domain.

As apposed to going into the never ending implementation not-what-we-were trying to solve weeds.

Re: Lean proved this program correct; then I found a bug

#68

Post by ajaystream »

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.

Re: Lean proved this program correct; then I found a bug

#69

Post by Animats »

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.

Re: Lean proved this program correct; then I found a bug

#70

Post by minimaltom »

grg0 wrote: post #61
minimaltom wrote: post #35

Earlier quoted context omitted.

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 pe…

Nobody with experience in the field advertises formally-verified software like that, and it is understood that the spec may as well be wrong. It is also understood that the non-verified parts may have bugs (surprise). There is no news here.

Unless "with experience in the field" == academia, disagree. In particular I remember the early discourse & hype around Wireguard, it was discussed as if perfection was an achieved outcome.
Post reply on HN