Link to how SQLite is tested, for anyone who's curious:
https://www.sqlite.org/testing.htmlThere'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).
[1] https://www.hyrumslaw.com