Interestingly, though, you can have some runtime checking with Dafny as well as the formidable dependent type checking and formal verification that happens at build time.

That means that most of the proof can be done ahead of time with just some loose ends verified using an SMT prover at runtime.