Doesn't TDD basically provide a spec? Write a test, then let the AI generate a program that passes the test. If the program is still buggy, you didn't write sufficient tests.
I'd be more curious to see an AI write tests...
If you go trough the easiest path, you just need to write the program and compare the results with the AI's ;)
But if you go on a case by case basis, your work will grow exponentially with the program size, not a mere 2x.
Static types also specify universal properties, which is why tests can't replace types, even in theory. But tests+types could be a type of spec.
Developing an AI that can infer a simple, tasteful set of general rules (and suitable types) from a small set of test cases is certainly hard but not theoretically impossible.
Automated tests are generally not practical for proofing program correctness. Why would you expect them to be sufficient as a specification format?
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.
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.
So I started tinkering with the concept, and I've got a bit of a start on it here:
https://github.com/michaelmelanson/autocoder
What's there is very rudimentary. The main class is a good place to start.
Basically I'm building up a library of transformations that can describe solutions to kata problems (the 'word wrap' one currently). The next step is to create a search algorithm to derive an ordered sequence of transformations from that library to pass an ordered sequence of tests.