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.
Issues
Bounty
There is a FOSS Factory bounty (p276) on some of these tasks.