Re:AlphaProof Code
by tsimionescu on Wednesday November 11, 2026 @04:16AM
(#50451242)
Have you ever looked at seL4 sources? I think that it might make you temper your expectations on what formal verification can practically achieve.
Specifically, seL4 formal verification took multiple (5+?) years by computer science PhDs treating it as novel research. And it's less than 50k lines of code total (might have actually been around 20k, if I remember correctly?), excluding the proof, with no dependencies at all outside the CPU.
Now look at Linux, or at Angular, or at any other piece of code you actually care about, and you'll see that even if we assumed simple linear scaling (which is obviously not a safe assumption as complexity increases rapidly with size), and even if LLMs can 10x the productivity, you'd still need decades or a team of dozens or hundreds of PhDs.
And also consider how much of that effort would have had to be redone when Linux added io_uring, for example.
Specifically, seL4 formal verification took multiple (5+?) years by computer science PhDs treating it as novel research. And it's less than 50k lines of code total (might have actually been around 20k, if I remember correctly?), excluding the proof, with no dependencies at all outside the CPU.
Now look at Linux, or at Angular, or at any other piece of code you actually care about, and you'll see that even if we assumed simple linear scaling (which is obviously not a safe assumption as complexity increases rapidly with size), and even if LLMs can 10x the productivity, you'd still need decades or a team of dozens or hundreds of PhDs.
And also consider how much of that effort would have had to be redone when Linux added io_uring, for example.