>> There are also performance characteristics that are part of an informal spec.

They are not informal AFAIK - https://github.com/PGPerfFarm. A lot of these heavy duty OS projects have explicit Perf testing/nighlites (see Lucene's at https://benchmarks.mikemccandless.com/)

If you are saying the PG regression suite doesn't cover these perf tests - that is fair. I consider perf to be part of the "regression framework" generally.

>> How do you know your new tests are right? That the new behavior is right?

This is a more generic question in the LLM world. Reliable verifiers is what drives LLM loops. If you don't have these, you have no idea if you are actually making progress or you just generated code that returns 42 for every question. You needs something to actually ground the LLM output against. For existing features, the reliable verification is the existing regression/perf suites. For new features, the regression/perf suites should expand to fit. There are ways to go at this that range from ad-hoc (line/branch coverage) to fully formalized (verification-aware languages like Dafny).