GenDB-V：AI 生成、形式化验证的数据库引擎
康奈尔大学的研究者提出了 GenDB-V，一个让 AI 智能体为特定硬件与工作负载合成数据库引擎、并对正确性做形式化验证的系统。它引入 SQLSpec 形式化 SQL 语义，联合合成高速代码与模块化证明；在 TPC-H 与 SEC-EDGAR 测试中，已验证的模板实现比 DuckDB 和 Umbra 快 22.0–61.3 倍（几何均值）。它之所以重要，是因为把大模型代码合成与形式化保证结合起来，直面了 AI 生成系统软件长期以来的正确性难题。
报道来源
- Hacker News (AI)2026-11-07 20:54