形式的検証と証明支援系

形式的検証とは、ソフトウェアがその仕様を満たしていることを、機械で検証された数学的証明によって確立することであり、証明支援系は、そのような証明を構築し検証するためのツールである。

Definition

形式的検証とは、システムが形式仕様を満たすことを厳密に機械で検証された証明を構築することであり、証明支援系とは、ユーザーがそのような証明を開発し、その妥当性を機械的に検証するのを助けるソフトウェアである。

Scope

このトピックでは、演繹的検証と対話型定理証明について扱う。具体的には、型理論または高階論理に基づく証明支援系（Coq、Isabelle、Lean、Agdaなど）、信頼できる証明のためのLCFアプローチ、命題と型の対応関係、証明の自動化とタクティクス、およびコンパイラやオペレーティングシステムカーネルを含む画期的な検証済み成果物についてである。

Core questions

• 完全な機能的正確性をどのように証明し、機械で検証できるのか？
• 証明支援系はなぜ信頼できるのか、そして信頼できる計算基盤とは何か？
• カリー＝ハワード同型対応は、証明とプログラムをどのように結びつけるのか？
• コンパイラやカーネルのような実際のシステムを検証するには何が必要か？

Key theories

信頼できる証明のためのLCFアプローチ

ゴードン、ミルナー、ワズワースのエディンバラLCFは、すべての定理が通過しなければならない小さな信頼された証明カーネルを導入した。これにより、複雑な自動化であっても不健全な証明を生成することはできない。

検証済みコンパイラ (CompCert)

ルロワのCompCertは、証明支援系で正しさが証明されたCコンパイラであり、生成されたコードがソースプログラムのセマンティクスを洗練するという機械で検証された定理を持つ。

検証済みオペレーティングシステムカーネル (seL4)

クラインらは、seL4マイクロカーネルの機能的正確性に関する機械で検証された証明を作成し、低レベルシステムソフトウェアのエンドツーエンド検証を実証した。

Clinical relevance

機械的検証は、重要なソフトウェアに対して利用可能な最高の保証を提供し、テストに基づく信頼性ではなく、証明された保証を備えたコンパイラ、カーネル、および暗号ライブラリを生成する。証明支援系は、数学そのものを形式化するためにもますます使用されている。

History

対話型定理証明は、1970年代のエディンバラLCFに始まり、そのMLメタ言語と信頼されたカーネルが後のシステムを形成した。CoqやAgdaのような型理論に基づく支援系や、Isabelle/HOLのような高階論理システムは、その後の数十年で成熟し、CompCertコンパイラ（2009年）やseL4カーネル（2009年）といった画期的な検証済み成果物で頂点に達した。

Debates

検証のコストと得られる保証の比較

大規模システムの機械で検証された証明を構築するには膨大な労力が必要であり、完全な検証が正当化される場所と、より軽量な方法で十分な場所、そしてどの程度の証明を自動化できるかについて議論が巻き起こっている。

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

証明支援系とは何か？

証明支援系とは、ユーザーが対話的に形式的証明を構築し、システムがすべてのステップを機械的に検証するソフトウェアである。これにより、完成した証明は、小さく厳密に精査されたカーネルに至るまで信頼できるものとなる。

プログラムの検証は、テストとどう違うのか？

テストは選択された入力に対する動作をチェックし、バグの存在を明らかにすることしかできないのに対し、形式的検証は仕様で許容されるすべての入力に対する正確性を証明し、指定されたエラーの不在を確立する。