Formal verification techniques

Posted Sep 11, 2025 8:06 UTC (Thu) by DemiMarie (subscriber, #164188)
In reply to: And then there's runtime options ... by willy
Parent article: How many ways are there to configure the Linux kernel?

Search-based approaches to formal verification fail to scale, and I believe it is for exactly this reason. Interactive theorem proving *can* scale, but it is still quadratic in the size of a module. Linux is a quite modular program, but I expect the proof effort would be in the hundreds of billions of dollars, if not trillions.