|
| ▲ | corysama an hour ago | parent | next [-] |
| 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... |
|
| ▲ | benlivengood an hour ago | parent | prev [-] |
| 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 an hour ago | parent [-] | | 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. |
|
