Forall：仕様駆動型AIコーディングと形式検証

Astrioチームは、仕様駆動型のAIコーディングエージェント「Forall（∀）」を正式にリリースしました。このツールは、開発者が記述した仕様に基づいてコードを生成すると同時に、機械で検証可能な形式証明を自動的に付与します。ソフトウェアの信頼性を高め、論理的なバグを削減することを目的としています。

Forallには2つの利用方法があります。1つ目はフル機能のCLIエージェントをインストールする方法で、ターミナル上でコード作成、仕様策定、証明生成の全てを完結できます。インストールは curl -fsSL https://forall.astrio.app/install.sh | bash を実行するだけで完了し、初回起動時にForallアカウントまたはOpenAI/OpenRouterのAPIキーを設定します。2つ目はCLIをインストールせず、MCP（Model Context Protocol）を介してCursor、Claude Code、Codexなどの既存IDEに統合し、リモート検証サービスだけを利用する方法です。利用者はForallダッシュボードでAPIキーを作成し、MCPクライアントに設定を追加します。

現時点ではTypeScript、Java、Rustの3言語に対応しており、コミュニティの要望に応じて言語を拡大する予定です。プロジェクト全体はApache-2.0ライセンスで公開され、GitHub上でホスティングされています。AstrioはDiscordとXのコミュニティも提供しており、開発者同士の交流を促進しています。GitHub上では現在160のスターと21のフォークを獲得しており、v0.1.0がリリースされています。Forallの核心理念は、開発者が仕様を記述することでコード生成を駆動し、同時に機械チェック可能な証明を自動生成することにあり、これによりソフトウェアの正確性と開発効率を大幅に向上させることを目指しています。