Discussion

lf-lean: The frontier of verified software engineering

ngruhn: Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.

benlivengood: Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.

ngruhn: Not saying this is useless. But that article reads like they made some kind of breakthrough in automatic software verification. But is sounds like they rather ported a tutorial test suite from Go to Rust with AI and the tests are still passing.

corysama: I believe what they are bragging about is not the translated proofs, but the process of doing the translation.> produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators...