Re:AlphaProof Code
by kylestanfield on Tuesday November 10, 2026 @05:44PM
(#50447360)
That’s true, but the theorem prover still needs a model of your code to check the theorem against. So how do we know it’s checking the theorems against an accurate model.
Say, no crashes, no dead or livelocks, O(n log n) in the size of the input, same number of instructions executed & memory accessed no matter what the encryption key is, etc etc.
These type of theorems are significantly smaller than the source code, pretty re-usable across different applications, and extremely useful properties.