I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it.
https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.
It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them.
https://arxiv.org/pdf/2304.10558
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?"