用 Quint 形式化验证 SQLite，发现 10+ 个 Bug

Turso 团队在加固其基于 SQLite 的分布式数据库时，使用 Quint（一种形式化规范语言）对 SQLite 的并发控制逻辑进行建模和模型检查，发现了超过 10 个真实 Bug。这些 Bug 涉及竞态条件、事务隔离违规和索引损坏等深层问题，传统测试难以覆盖。

Quint 通过将 SQLite 的内部状态机抽象为 TLA+ 风格的规范，再借助模型检查器穷举所有可能的状态路径，从而在开发早期捕获逻辑错误。该工作展示了形式化方法在数据库内核质量保障中的实用价值。