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.
benlivengood1 day ago
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.
ngruhn1 day ago
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.
corysama1 day ago
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...
akkad331 day ago
This website is asking me for permissions on my phone. Why?
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.
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.
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.
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...
This website is asking me for permissions on my phone. Why?