There are plenty of proof systems that can handle floating point? The proof doesn't happen during execution...