And that's why my point was that we don't know how to come up with heuristics: because we currently don't.
Edit: if you mean that we can probabilistic-recall all those heuristics, that's not right. Because such heuristics are tacit knowledge that is very difficult, maybe even impossible, to articulate with enough accuracy to reproduce in a computer. We certainly can't get LLMs to learn them from the web because the web doesn't have text that explains e.g. how to control your muscles to climb a tree.
But this is a thread about a formal verification language, and in this area "just throwing non-deterministic proofs at it until something sticks" works kinda well.
And you just sort of said that something getting "figured out" by a random process with selection can't be a heuristic, as it has to be "novel" (whatever that means). Well, then unfortunately we have to exclude animals from that list as well, because if you read it again, that's pretty much how evolution works.