I think they mean something like what proof assistants like Cog and Irdis do. ATS is another language that enables proofs, and it's more geared to the systems programming use case, as it's similar to C.

Note that unit tests prove only that the code works for those inputs and those code paths tested. Mathematical proofs are supposed to be exhaustive.