PDD（証明駆動開発）とは、システムの正しさを保証するために、形式手法や数学的証明の使用を重視するソフトウェア開発のアプローチです。この用語は、テスト駆動開発（TDD）や行動駆動開発（BDD）のような他の開発方法論ほど広く使われたり標準化されてはいませんが、この概念が示すものは、ソフトウェア開発の特定の分野、特に高保証または安全が重要なシステムを扱う分野で重要な役割を担っています。
PDDでは、コードを書く前に、開発者はソフトウェアの形式的な仕様を作成します。これは、ソフトウェアが何をすべきかを数学的または論理的な用語で表現した、詳細で明確な記述です。そして、開発者が提案するソリューションが、あらゆる可能なシナリオにおいてこれらの仕様を満たすことを示すための証明を作成します。
例えば、交通量の多い交差点で信号機を制御するシステムを考えてみましょう。仕様の1つに、「交差する交通の流れに対して青信号を許可してはならない」というものがあるとします。そして、設計されたソフトウェアが、どのような状況下でも本当にこの条件を守ることについて証明を構築します。
証明の構築後、実際のコードは証明を反映するように書きます。こうして完成したソフトウェアは、その挙動が仕様に適合することが数学的に証明され、期待通りの動作をすることが保証されます。
PDDはコストが高く複雑なため、一般的なソフトウェア開発ではあまり使われませんが、航空宇宙、原子力、医療システムなど、失敗のコストが非常に高い特定の領域では不可欠なものです。