深度分析
BODHI：以結構化領域知識提升 LLM 在 OSV-Bench 形式規格生成的準確度
作業系統核心形式驗證需精準規格，但手動撰寫昂貴。BODHI 以結構化 C→Python/Z3 翻譯指南擴充 few-shot prompt，分離前置檢查與後置狀態更新等關切點，並示範 15 類翻譯模式。實驗在 OSV-Bench 上顯著提升多款模型 Pass@1，顯示領域知識注入可實質改善規格生成。
Z3
神經符號聚合
結合 LLM 語意抽取與 Z3 的加權 MaxSAT 道德判斷聚合框架
本研究提出一套神經符號聚合框架，將 Reddit r/AmItheAsshole 上的道德評論透過大型語言模型抽取成可解釋的邏輯謂詞與信心權重，並以加權最大可滿足度（Weighted MaxSAT）方式交由 Z3 求解器求解，產生邏輯一致的最終判決。
深度分析
用 Z3 位元向量建模：COBALT 對 C/C++ 沙盒算術溢位的形式化檢測
2026年ClaudeMythos沙盒逃逸揭示前沿模型隔離的算術弱點。提出COBALT一套基於Z3的預部署形式驗證引擎，用位元向量對C/C++算術操作建模並求解SAT/UNSAT。工具能在生產代碼庫重現可觸發模式並回傳具體見證，部署阻擋成為可行控制點。