It looks like they have an unverified compiler, which assuming correctness of the compiler code, will produce a proof of correctness for each program it compiles. This is significantly less cool and useful than proving that the compiler itself is correct.