With property-based testing one can describing the behavior over the entire domain(s) of valid inputs. Sampling is used to draw a set of cases to actually test, up to a certain number of test. Knowledge about boundary conditions in the domain can help catching failures earlier, though plain random seems to be pretty darn effective (at least for code written by humans). Candidates with dead code should maybe be punished. Candidates with higher complexity should maybe be punished.

Software produced by a typical business app developer is not provably correct either. TDD of AI generated code could not hope to produce something more correct. As your tests get better, so would the software produced both by the human and the AI.

For your add(int32, int32) function: While an AI-generated implementation is not provably correct unless the test contains 2^64 inputs, I think it's pretty likely that a correct implementation would in fact be generated pretty quickly.

I don't think it's as likely as you assume. Let's say you ask the computer to implement your adder, and you feed it the results of a few dozen, or a few hundred uint32 a + uint32 b = uint32 c operations. By coincidence, however, in all of those operations, every time bit a[14] is zero, bit c[26] also happens to be zero. The computer may produce an implementation which assumes this is always the case. The computer may also reason it does not need to look at some of the input bits, if say, for all of the tests, bit b[2] == bit b[16].

It may seem that a solution with assumptions like those are more complex than a simple addition operation, and thus the computer will find the addition solution first, but "simple" is a matter of perspective. Addition requires a logic cascade through the entire number, since the carries of the lower bits must be passed to the upper bits, which requires a critical path equal to the entire length of the inputs/outputs. In searching for an implementation which satisfies the few dozen/hundred test cases you feed it, making assumptions like those in the first paragraph can drastically shorten the critical path, and require far less logic since it's ignoring much of the input. Thus algorithmically, the addition operation may be seen as more complex.

(BTW, I don't think it's that simple either. Just pointing out that TDD is a possible approach to avoiding the infinite recursion of specs-are-just-programs-in-a-higher-level-language.)