Post #1172683
2026-04-14 01:25 UTC
Replies (8)
-
@danvolchek@mastodon.social 2026-04-14 01:55
@regehr i don't see anything interesting here they didn't do anything besides give money to anthropic in exchange for extremely inefficient fuzzing great? does that count as doing something now? worth a blog post? ahhhhhhhhhhhhhhhhhhh
-
@dpiponi@mathstodon.xyz 2026-04-14 02:03
@regehr I'm a n00b at this stuff but I'm unsurprised. I learnt a little Lean years ago and returned to it recently. I got Codex to generate a proof of a standard theorem. It involves enumeration. It used native_decide to do the enumeration. This is no longer a proof in the Lean kernel. I have to trust the Lean runtime now. That's a whole new level of trust I don't have yet. So thank you for this pointer to precisely what I was worried about!
-
@Lee_Holmes@infosec.exchange 2026-04-14 02:28
@regehr I thought the takeaways were cool: what was "proven" was remarkably secure, the edges around it had some issues. And the proof runtime 🤦 Great example of using two premier security technologies.
-
@rst@mastodon.social 2026-04-14 02:56
@regehr It didn't find bugs in *the portion of the code that was formally verified*. Which left the parser (out of scope for the proofs, but obviously part of the attack surface... oops!), and... the lean runtime itself.
-
@cfbolz@mastodon.social 2026-04-14 06:55
@regehr I love this post, and I hate how much nonsense discourse there is on hn about it 🙄 (I know, what did I expect)
-
@Filip0x0A@mastodon.social 2026-04-14 14:32
@regehr If I may ask, any recommendations on what I should consider when I am interested in applying formal methods for software security in practice? For example do you think it makes sense to get a math degree? (in addition to IT) Or just in general, what do you see as viable step(s) towards working on real-world application of formal methods? Asking because I am not even sure what I should take into account when considering this.
-
@purp@mastodon.social 2026-04-14 22:53
@regehr loved the article; while ill never write formally verified code, love stretching my mind around it and also seeing the validation/verification parallel to the LLM “did you understand what you wanted well and completely enough to describe it to the robot?”
-
@GeorgWeissenbacher@fediscience.org 2026-04-15 09:00
@regehr you state that someone takes formally verified code and finds real problems. However, the blog post states that the problems were found in the *non-verified* code: the parser and the Lean runtime. I quote from the blog post: "The positive result here is actually the remarkable one. Across 105 million executions, the application code (that is, excluding the runtime) had zero heap buffer overflows, zero use-after-free, zero stack buffer overflows, zero undefined behaviour (UBSan clean), and zero out-of-bounds array reads in the Lean-generated C code." Arguably, the denial-of-service was a problem in the verified code, but: "[t]he denial-of-service was a missing specification". Which, as I posted elsewhere, is a validation problem and not a verification problem.