Turso 以 Quint 形式驗證在 SQLite 找出逾 10 個潛伏 Bug
Turso Engineering Blog · 2026-05-19
Turso 工程師 Pavan Nambi 以 Quint（基於 TLA+ 的形式驗證工具）對 SQLite C API 建模，在數十年充分測試的資料庫中找到逾 10 個原本未被發現的 bug，其中包括資料損壞路徑與 crash。
方法論：不建模實作，只建模 API 合約
Quint 結合 TLA+ 的時序邏輯與現代型別系統，讓形式驗證更易上手。Nambi 的關鍵設計決策是不嘗試建模 SQLite 的內部實作，而是只建模其公開 C API 的合約（preconditions、postconditions、合法的呼叫序列）。這使模型規模可控，且直接對應到應用程式開發者的使用方式。
流程：在 Quint 中定義 API 合約 → 自動生成執行序列（execution traces）→ 在真實 SQLite 上跑這些序列 → 比較預期行為與觀察行為。
發現的主要 Bug
sqlite3_deserialize()crash：在活躍讀取交易期間呼叫 deserialize 應返回SQLITE_BUSY，但實際上導致 crash- EXISTS 轉 join 優化的 LIMIT/OFFSET 錯誤：查詢最佳化器將
EXISTS子查詢轉換為 join 時，在特定情況下錯誤地套用了 LIMIT/OFFSET 語意 - Backup/deserialization 交錯觸發 crash：備份與反序列化操作並發執行的特定時序導致記憶體錯誤
- xfer 最佳化繞過完整性檢查：快速資料轉移路徑跳過了本應執行的約束驗證
- 多個函式中的 NULL pointer 問題及型別/約束處理錯誤
意義
SQLite 是地球上執行次數最多的資料庫引擎，同時也是被測試最徹底的開源軟體之一。此研究顯示，形式驗證可以探索到傳統 fuzzing 與模擬測試難以覆蓋的規格空間——特別是對 API 呼叫序列的合法性約束。Turso 的 libSQL（SQLite 的 fork）已將這些發現上游回報給 SQLite 官方維護團隊。
ClickStack April 2026：SQL 告警、日誌 Schema 重設計與屬性 Map 加速
ClickHouse Blog · 2026-05-19
ClickHouse 於 2026 年 5 月發布 ClickStack April 2026 更新，重點聚焦三個方向：直接從 SQL 查詢建立告警、otel_logs 預設 schema 的效能重設計，以及 OpenTelemetry 屬性 Map 的直接讀取最佳化。
SQL-Powered 告警
新的告警系統允許使用者直接在 ClickHouse SQL 查詢結果上設定告警條件，支援的場景包括 rolling baseline 比較、百分位數漂移偵測、分組異常檢查與歷史資料對照。支援的比較運算子擴充至 >、≥、<、≤、=、≠、BETWEEN，告警歷史紀錄與確認（acknowledgment）控制也已整合進 UI。
otel_logs Schema 重設計
預設的 otel_logs 資料表 schema 進行重大重構，圍繞 ClickHouse 的 text index 能力重新設計主鍵結構，採用五分鐘時間桶配合服務名稱作為排序鍵。官方聲稱對常見搜尋與過濾工作負載有顯著加速，但具體倍率標記為 "Nx"（未揭露精確數字）。
屬性 Map 直接讀取優化
OpenTelemetry 屬性（attributes）在 ClickHouse 中以 Map 型別儲存，傳統的 map lookup 查詢需要掃描整個 map 鍵值對。新的優化將 map lookup 改寫為 indexed array 搜尋，對屬性過濾操作達到 1.4 至 10 倍的效能提升，範圍取決於屬性的基數與查詢模式。
其他改進
- Autocomplete：改用 materialized view rollup 實現元資料快速探索，加入頻率排序
- Heatmap 視覺化：從 Event Deltas 移至通用圖表系統，可在 dashboard 直接展示延遲分布