How we used Quint to find over 10 bugs in SQLite while hardening Turso

I have been quite interested in Turso for some time now, as innovating on sqlite is cool, and seeing them apply DST and formal verification methods to some of these problems is extra cool.

I am a bit amused at the difference between the quite professional sounding tone of "we are working with the SQLite team to validate [our findings]" and then clicking through to see that this means a few forum posts and bug reports that have a distinctly different tone. Definitely cool to see bugs getting fixed and open source community in action though, even if the findings are mostly minor inconsistencies in the c api and some documentation mismatches.