I'm not sure how a "spec with floats" differs from a spec with networks, RAM, 64-bit integers, multi-level cache, or any computing concept, none of which exists as a primitive in mathematics. A floating point number is a pair of integers, or sometimes we think about it as a real number plus some error, and TLAPS can check theorems about specifications that describe floating-point operations.
Of course, things can become more involved if you want to account for overflow, but overflow can get complicated even with integers.
Of course, things can become more involved if you want to account for overflow, but overflow can get complicated even with integers.