形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証は、システムにプログラミングの誤りがないことを保証する既知の唯一の方法である。“”ACMシンポジウムで発表された論文の要約から
