astrio-labs/forall

解決する課題

Forallはソフトウェアレビューおよび検証のボトルネックに対処します。テストや型システムは一定程度の保証を提供しますが、コードが実際に意図された機能を実行していることを証明することはできません。Forallは言語モデルを活用して、形式的検証への障壁を低くし、証明者がコードの正しさを保証するために必要な仕様、契約、不変条件の記述という繰り返し作業を自動化します。

動作方法

ForallはAIをソフトウェア開発ライフサイクルに統合し、正しさの証拠を生成します。各要件に対して4段階の証拠を提供します：

1. 仕様の追跡: 要件がコードにリンクされています。
2. 性質の検証: ジェネレータが多数の入力に対して反例をチェック（統計的証拠）。
3. 契約化: コード用の機械検証可能な契約が記述されています。
4. 証明済み: 形式的な証明者が契約の義務が満たされていることを確認しています。

対象ユーザー

IEC 62304やDO-178Cなどの基準に準拠するミッションクリティカルまたは規制対象のソフトウェアを開発する開発者向けに設計されています。トレーサビリティと形式的正しさ証拠の要求が厳しくなる分野に適しています。

特徴

• 二重インターフェース: クリック可能なコードエージェントCLIとして利用可能、またはCursorやClaude Codeなどのクライアント内で使用可能なMCP（Model Context Protocol）サーバーとして利用可能。
• 多言語対応: TypeScript、Python、Rust、Java、Cをサポート。各言語での検証能力は異なります。
• 柔軟なモデル統合: ホステッドモデルまたはBYOK（Bring-Your-Own-Key）を用いてOpenAI、Anthropic、Google Gemini、Azure、Amazon Bedrockに対応。
• 証拠に基づく評価: 単なる合格/不合格ではなく、機械が生成した最も強力な証拠に基づいて要件を評価します。