Re:AlphaProof Code
by guenthert on Wednesday November 11, 2026 @04:16AM
(#50451238)
> it's now fairly easy to get an AI generated proof that your code follows the spec
It's my understanding that automatic tools were able for a while already to verify whether a given system (code or otherwise) adheres to a given formal specification (at one point after the Pentium bug debacle AMD had its FPU proven, there are variants of the L4 microkernel which were proven, etc.).
The (great) challenge remained to create a formal specification from something humans can write and understand. Isn't that were LLMs come in? And isn't that were the current trust gap remains?
It's my understanding that automatic tools were able for a while already to verify whether a given system (code or otherwise) adheres to a given formal specification (at one point after the Pentium bug debacle AMD had its FPU proven, there are variants of the L4 microkernel which were proven, etc.).
The (great) challenge remained to create a formal specification from something humans can write and understand. Isn't that were LLMs come in? And isn't that were the current trust gap remains?