Metamorphic testing with Lean4-verified mutations finds compiler miscompilations (opens in new tab)

Hunting compiler miscompilations on smart-contract platforms with differential and metamorphic testing, using mutations proven equivalence-preserving in Lean4 — including real-world findings, some rewarded with bug bounties.