Using LLM-based Verification to Eliminate Bugs in Linux's Network Stack
5 points by kirancodes
5 points by kirancodes
Fortunately, LLMs are increasingly capable of verification too, pointing toward a future where critical software infrastructure is secure by construction
This is a complete non-sequitur, isn't it? "Secure by construction" is different to "verified after construction", surely
If it helps you to have the implication chain spelt out, LLMs are good at verification, ergo we are heading towards a future in which software is developed and released with proofs, i.e correct by construction.
software is developed and released with proofs, i.e correct by construction.
I had always thought "correct by construction" meant that the models were produced before the code, and that the code was then produced according to the model in such a (mechanical) way that it certainly satisfied the model. I.e. the "by construction" part refers to the fact that the code is constructed in such a way that it is known to be correct. Producing a proof after the fact may achieve the same result, but it's not the same technique.