税法を定理証明支援系 Lean で書いて、プロダクト実装を「全入力で」確かめる

DRANK

税の計算が法令どおりかは、ソフトウェアテストでは人が選んだテストケースの分しか確かめられません。本番で動いている税計算を、定理証明支援系 Lean と AI エージェントで、法令から起こした仕様とすべての入力で突き合わせました。一致の確認と、選び方で税額が変わる箇所の洗い出しの方法を紹介します。