Show HN: 形式検証を用いた要求工学
オープンソースの形式手法システム「Fizzbee」を基にした新アプリを発表。与えられたプロンプトに対し、高品質なフォローアップ質問を実施し、形式的仕様に変換して要件のギャップを特定。最終的にコーディングエージェントが利用可能な仕様書を生成し、少ないイテレーションで正常動作するコードを実現する。
背景メモ
- Fizzbee は、システムの振る舞いを数学的に検証する「形式手法（formal methods）」を手軽に使えるようにするオープンソースツール。今回新たに公開された fizzbee.ai は、その技術を応用し、LLM（大規模言語モデル）を使ったコーディングエージェント向けの「要求仕様書（specification document）」を自動生成するWebアプリ。
- 通常、コード生成AIに「○○を作って」と依頼すると、抜け漏れや矛盾があってもそのままコード化され、後でバグになる。Fizzbee.ai は、入力を形式検証可能な仕様に変換してギャップを洗い出し、その上でエージェントが迷わない精密な指示書を出力する。
- 「形式手法」は航空宇宙や金融などミッションクリティカルな分野で使われる高信頼性技術だが、敷居が高い。Fizzbee は TLA+（Amazon が開発した形式仕様言語）に似た独自の簡易言語（DatomicスタイルのFizzBee DSL）を採用し、エンジニアが普段使いできるよう設計されている。