specula-org/Specula

何を解決するか

Speculaは、並行および分散システムにおける深い、複雑なバグを発見する難しさに対処します。このようなシステムの形式仕様を手動で記述するのは時間と労力がかかる上、専門的な知識を要するため、大規模なオープンソースプロジェクトに形式検証をスケーリングするのは困難です。

どう動くか

SpeculaはAIコーディングエージェントを用いて形式検証パイプラインを自動化します。プロセスは以下のステップに従います：

1. 分析と仕様作成：コーディングエージェントがシステムのソースコードを読み取り、正しさの性質（不変条件）を推論し、TLA+で形式仕様を記述します。
2. モデル検査：システムはこれらの仕様をモデル検査して、不変条件の違反の可能性を特定します。
3. バグの再現：違反が検出された場合、エージェントは反例を分析し、実際のコードレベルでバグを再現します。

「Auto Mode」でエンドツーエンドの実行が可能であり、また「Interactive Mode」では、code-analysis、spec-generation、bug-confirmationなどの特定のスキルを順番にトリガーできます。

対象ユーザー

並行または分散システムの開発に取り組むソフトウェアエンジニアや研究者向けです。形式仕様を一つひとつ手動で書くことなく、深いアーキテクチャ的または同期に関するバグを発見したい方におすすめです。

特徴

• 自律的な TLA+ 生成：LLMベースのエージェントを用いて実装コードを形式モデルに変換します。
• コードレベルでの再現：抽象的なモデル検査の違反と具体的なコードバグの間のギャップを埋めます。
• エージェント統合：Claude Code、Codex、Copilot CLI、OpenCode、Pi など、複数のコーディングエージェントをサポートします。
• 拡張可能なツールセット：トレースデバッグや仕様分析に使えるMCP（Model Context Protocol）ツールを含みます。