Formal verification (Wikipedia article) deals with formally reasoning about a program's correctness.

Especially in the field of DSLs, this is used for asserting program codes' correctness, as explained in Pierre-Evariste Dagand, Andrew Baumann, Timothy Roscoe. Filet-o-Fish: practical and dependable domain-specific languages for OS development. PLOS '09, October 11, 2009, Big Sky, Montana, USA., for example.

See also code analysis.



There is a FOSS Factory bounty (p276) on some of these tasks.