Full-stack verification is the new trend

This could be nice, but I expect that users of these systems will increasingly also have AI generate the contracts/annotations*/theorems that are being checked/proven/etc. Making a Verified with LEAN ✅ or whatever label generally meaningless. Oh well...

(Besides the fact that "uses AI" becomes the general starting point, and local optimum, for any technique in this space. I guess that's more of a personal problem if you don't want to work on AI)

*: Generating loop invariants would be awesome! Pre/postconditions of the public API less so.