Comment by malisper

I have a unique perspective on this as I've been working on rewriting and rearchitecting Postgres to solve a lot of the long standing issues Postgres has[0][1].

If I had to root cause why we're finding so many bugs now, I would attribute it to the limited Postgres test suite. AI is merely uncovering bugs that already existed. For the most part, Postgres relies on individual regression tests to test each feature. While regression tests are great for making sure features don't break (yes, SELECT 'Hello, World' LIKE '%Hello%' still returns true), they actually aren't that great hitting the edge cases (passing a string that's over 2MB to a specific function will trigger a buffer overflow and crash your DB). The main way Postgres has prevented bugs in the past has been by minimizing risky changes and having lots of human review. As we're learning now, there were lots of gaps that were not caught by the existing process.

While the Postgres team is skeptical of AI, I've had lots of success in using AI to scale more advanced forms of testing such as Deterministic Simulation Testing, differential coverage guided fuzzing, and formal verification. To put it in perspective, in the process of doing testing for pgrust, I've uncovered ~50 different bugs in core Postgres. The bugs I'm finding aren't through AI review, but are instead through using AI to do more advanced testing than regression testing. All of the techniques I'm using existed existed pre-AI, but aren't used in meaningful capacity as part of the core Postgres development.

Right now I'm going all in on formal verification. I wrote a compiler to translate C and Rust functions to Lean and am then having an LLM write a proof that the two functions are identical. So far I've been able to verify 10.5% of the codebases behave identically (10.5% = 67k/640k LOC of Postgres). I'm finding details as minute as a parsing function where Postgres trimmed spaces using isspace() and pgrust only trimmed ascii whitespaces. These aren't cases you would find with traditional regression testing or human review. The thoroughness of the types of bugs I'm finding is giving me confidence that that this is catching more bugs than any sort of manual testing could. I don't currently see any reason that I won't be able to scale up the formal verification to cover 100% of the codebase. The only issue is it takes a long time to do.

[0] https://github.com/malisper/pgrust

[1] https://malisper.me/the-four-horsemen-behind-thousands-of-po...