Tools like Alive have made translation validation habitual in LLVM development, where a proposed InstCombine rewrite is checked against a solver before it lands. We want this habit to extend, robustly, to the floating-point rewrites and the machine-learning formats (f8E4M3, f8E5M2, bf16) that modern hardware is increasingly adopting. For such tools to be trustworthy, we need two ingredients: a clear semantics for the operations being rewritten, and a solver whose answers we can trust. However, floating-point solvers are notoriously hard to get right, where every mainstream solver has been shown to admit soundness defects, and even the state of the art has untested corners: The Bitwuzla SMT solver rejects the ML formats unless built with --fpexp, an option its release notes label "use at your own risk". We therefore formally verify a floating-point solver in the Lean proof assistant, mechanizing the chain from the SMT-LIB floating-point semantics down to the bit-level circuits handed to a SAT solver, so formats like E4M3 and E5M2 are covered by the same proofs as float32. We evaluate on a benchmark suite lifted from InstCombine itself, by running the -O2 pipeline over its floating-point tests and translating the before/after programs into refinement obligations at small formats. The performance delta is acceptable, where we we certify 100 of 100 rewrites, and we are an order of magnitude faster than exhaustive enumeration (the only other sound option). Furthermore, our methods scale, as we have a 33.8× geomean slowdown of Bitwuzla on the large SMT-COMP problems, so verifying these small formats in a trustworthy fashion is entirely practical today. In this talk we explain the solver technology, and then ask the audience where to take it: we currently support bit-level IEEE reasoning, but we want clear semantics for fast-math, and a sense of what features our solver should add. Relatedly, we will explain the algorithms and tradeoffs Triton takes in its floating-point verifier, fpsan, and ask whether our initial pursuit into formally verifying this direction would be fruitful to expand.