formal verification

Formal verification checks, through logic and proof, whether hardware or software meets a mathematically defined specification. Unlike testing, which exercises only some inputs, it aims to show that a property holds in every case the specification covers. Common techniques include model checking and theorem proving.

It has long been applied where errors are costly, such as chip design, aerospace, operating system kernels and cryptography. In AI, it serves as a way to mechanically check code and mathematical proofs that models generate.

This entry is based on AIPOST articles and widely known facts. If something is wrong, please send us a correction request.