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.
Sorry this comment is so late; ATS is also interesting because it has linear types that allow compile-time resource tracking similar to Rust's ownership and lifetime tracking. If you use linear types you can opt out of the garbage collector. That makes it very attractive for systems programming, and in particular embedded systems. I believe there is a demo of ATS running on an Arduino of some sort.
I haven't had the time to learn it yet, though I would like to.
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.