At the risk of telling you something you already know, I’d bring to your attention for example property-based testing, probably most popularized by Hypothesis, which is great wud I recommend, but by no means the only approach or high-quality implementation. I think QuickCheck for Haskell was around when it got big enough to show up on HN.
Just in case any reader hasn’t tried this, the basic idea is to make statements about code’s behavior that are weaker than a totally closed-form proof system (which also have their place) stated as “properties” than are checked up to some inherently probabilistic bound, which can be quite useful statements.
The “canonical” example is reversing a string: two applications of string reverse is generally intended to produce the input. But with 1 line of code, you can check as many weird Unicode edge cases or whatever as you have time and electricity.
I know this example seems trite, but I met this because some hard CUDA hackers doing the autodiff and kernels and shit that became PyTorch used it to tremendous effect and probably got 5x the confidence in the code for half the effort/price.
It doesn’t always work out, but when it does it’s great, and LLMs seems to be able to get a Hypothesis case sort of, closer than starting from scratch.