The problem is that effort to do formal verification goes exponential beyond a certain point.
seL4 is around 10-12 KLoC, and it took a decade of effort from multiple people to make it happen.
At the size of SQLite, especially where they have to operate on platforms with different behavior (as an OS, seL4 is the platform), formal verification is just too much effort.
All that said, your reaction is totally understandable.
There's also an interesting thing where formal verification requires a formal specification, which afaik there isn't one for SQLite. One of the toughest problems that someone would run into trying to put together a formal specification for code as widely deployed as SQLite boils down to Hyrum's Law[1]: on a long enough time scale, all observable behaviours of your system become interfaces that someone, somewhere depends on.
That massive suite of test cases isn't a formal specification but given that it achieves 100% branch coverage that implies to me that it:
- pretty tightly bounds the interface without formally specifying it
- also pretty tightly constrains the implementation to match the current implementation
Which, when you have as many users as you do with SQLite, is probably a fair way of providing guarantees to your users that upgrading from 3.44.0 to 3.45.1 isn't going to break anything you're using unless you were relying on explicitly-identified buggy behaviour (you'd be able to see the delta in the test cases if you looked at the Fossil diffs).
Also a formal specification can have bugs. Formal verification checks that the code matches the spec, not that the spec implements all desired behaviors and no undesired behaviors.
You're right, though it's worth noting that you can also use formal verification to verify properties about the specification! For example you can verify that a security system doesn't allow privilege escalation.
Yep, though of course it's still on you to remember to verify everything you care about. Actually writing out all your requirements in a formal (or just programming) language is the hard part of programming.
seL4 is around 10-12 KLoC, and it took a decade of effort from multiple people to make it happen.
At the size of SQLite, especially where they have to operate on platforms with different behavior (as an OS, seL4 is the platform), formal verification is just too much effort.
All that said, your reaction is totally understandable.