> This is why "is my testing comprehensive?" is actually an open-ended problem that, in the limit, is just as hard as formal verification.

Well said! I learned about PBT in the first place because I watched a talk where the speaker referenced the story of foundationDB. Super interesting stuff. If anybody wants a link I can dig it up