specula-org/Specula

解決的問題

Specula 解決了在並行與分散式系統中發現深層、複雜 bug 的困難。手動撰寫此類系統的正式規格耗時且需專業知識，使得形式化驗證難以擴展至大型開源專案。

工作原理

Specula 使用 AI 編碼代理來自動化形式化驗證流程。該過程包含以下步驟：

1. 分析與規格生成：編碼代理讀取系統的原始碼，推論正確性屬性（不變量），並以 TLA+ 寫出正式規格。
2. 模型檢測：系統對這些規格進行模型檢測，以識別不變量可能被違反的情況。
3. Bug 復現：當發現違反時，代理會分析反例，以在實際原始碼層級重現該 Bug。

它可在「自動模式」下實現端對端執行，也可在「互動模式」下，由使用者依序觸發 code-analysis、spec-generation 和 bug-confirmation 等特定技能。

適用對象

專為希望在不手動撰寫每個正式規格的情況下，發現並行或分散式系統中深層架構或同步 Bug 的軟體工程師與研究人員設計。

主要亮點

• 自主生成 TLA+：使用基於 LLM 的代理將實作原始碼轉換為形式化模型。
• 程式碼層級復現：彌補抽象模型檢測違規與具體程式碼 Bug 之間的差距。
• 代理整合：支援多種編碼代理，包括 Claude Code、Codex、Copilot CLI、OpenCode 和 Pi。
• 可擴展工具鏈：包含 MCP（Model Context Protocol）工具，用於追蹤除錯與規格分析。