pgrust

ing 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...