Machine-Checked Trust for Agent-Built Hardware: LLM Agents Formally Verify Synthesizable Floating-Point Arithmetic

We report what we believe is the first formally verified, synthesizable floating-point arithmetic stack implemented and proved by LLM agents: first-class FP32, BF16, OCP FP8, and block-scaled microscaling (MX/NVFP4) data types and arithmetic operators for a hardware description language compiled to synthesizable SystemVerilog. The work was designed and directed by the authors; implemented and proved by LLM agents; and every functional-correctness claim is machine-checked. Agent-produced engineering can be trustworthy to the extent that its acceptance gates are: every functional-correctness artifact passes Lean's minimal trusted proof checker (with LRAT-certified SAT steps), SMT \texttt{unsat} verdicts with mutation-tested non-vacuity, exhaustive enumeration, or a structural netlist check --- gates that are binary, machine-decided, and independent of who or what produced the work. Every operator is described once against a single bit-vector IR rendered three ways --- SystemVerilog (the hardware), SMT-LIB (a formal model), and Lean~4 (a proof model) --- so the three artifacts cannot drift structurally by construction; the residual trust is the per-node syntax table, and the SystemVerilog side is itself machine-checked by a Yosys-to-SMT miter, and verification splits at the solver-tractability frontier: multiplier-free operators are proved exhaustively by SMT, while the SAT-hard FP32 multiply and fused multiply--add are proved correctly rounded in Lean, \code{sorry}-free (the BF16 and E5M2 \fma{}s implement a \emph{characterized} FP32-accumulating fusion instead; the E4M3 \fma{} is proved correctly rounded outright). Timing characterization drove a redesign of the \fma{} from an exact-wide reference to a bounded sticky-fold datapath that pipelines to $268$\,MHz, joined to the reference by a bit-exact equivalence proof over all $2^{96}$ inputs in which the shared multiplier cancels. The same discipline extends to low bitwidth FP8 (the E4M3 fused \fma{} is \emph{proved} correctly rounded outright) and to block-scaled operators whose pipelined datapaths carry their own machine-checked latency-equivalence --- a structural balance check, an uninterpreted-function wiring miter, and a Lean retiming lemma. Formal verification application is further extended to solver-closed system-level properties: certified absence of narrowing overflow, Gappa-checked error bounds, and a machine-checked pairwise-summation accuracy bound over the proven adder.