[curtisf]

Formal verification is explicitly NOT testing.

It is a method where a computer verifies a proof that the program adheres to its specification for _all_ inputs (subject to whatever limitations the particular method has).

Types are the simplest kind of formal verification, and with sufficiently advanced dependent type-systems, can be used to prove that programs obey arbitrarily complex specifications. However, this can be extremely laborious and requires significantly different skills than normal programming, so it is very rarely done in industry