> the repo being a regression harness is the useful part here No, the useful part is that it nails down actual unsound behavior with reproductions, not that it happens to be wrapped in a harness. A regression script is nice once you already have a bug, but it doesnt tell you much about whether the bug is real, minimized, or just a flaky test artifact. Here the point is the five PoCs and the fact that they still hit develop HEAD, the harness is just the packaging around that. Also, I dont think the tl;dr is burying the lead, the lead is still "soundness bugs". "Beyond the usual trust the prover workflow" is just saying this isnt a whitepaper about methodology, its a bug repo you can run against a build, which is exactly the right framing for something aimed at people who actually want to check the failure mode.