形式手法を用いてテストを生成したい

以前作成していたライブラリにて、致命的な論理バグがあった

Routingをするのにも関わらず、FFIの型変換ミスで必ずフォールバックがマッチしてしまう

coderabbitによるcode reviewは導入したが、対象療法感がある

LLMにそのまま実装とテストコードを書かせるとテストケースを八百長してくる

期待する振る舞いをLLMと合意のとれる形で定義し、テストコードの実装を強制する必要がある

gherkin

alloy