I only skimmed this paper, but it doesn't mention floating point (it's only modeling the FNN as a function on reals), and I don't think you can extract a working FNN implementation from an SMT-LIB or Z3 problem statement, so I think you have to take on faith the correspondence between the implementation you're running and the thing you proved correct.

But that's the actual problem we're trying to solve; nobody really doubts Kalman's proof of his filter's optimality.

So this paper is not a relevant answer to the question, "how would you prove an implementation of a Kalman filter is correct?"