Link to how SQLite is tested, for anyone who's curious: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html There's also an interesting thi

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