Has anyone done formal code proofs of D code. I've got an idea for a project that might need it and am wondering if anyone has any pointers/stories/etc.