ソフトウェアは、スマートフォンやコンピュータだけでなく、交通・金融・医療・エネルギーなどの社会基盤を支えています。一方で、大規模化・複雑化に伴い、その正しさや安全性を保証することはますます難しくなっています。本講演では、ソフトウェアが仕様どおりに動作することを数学的に保証するプログラム検証技術を基礎から概説します。また、C言語やRustを対象とした自動検証ツールの開発と、その基盤技術について紹介します。