The scope of what we can verify is still tiny. It worked well for "this program won't crash". It's really hard for cases like "this encryption is secure" or "this compression always decompresses to the same thing". But anything like "this GUI program that talks to an SQL database does what's expected" is basically impossible and we're not even close.

It's going to take way more than throwing a more advanced LLM at the problem to make any progress.