> Only the small and unimpressive programs can be checked exhaustively.

Even if you assume that statement is true, there are techniques other than exhaustive checking/model checking. Proof assistants/theorem provers/etc. like Rocq/Isabelle/Lean are quite capable of formally verifying programs without needing to exhaustively explore the search space.

I'd question the accuracy of that statement in general as well; model checkers like CBMC/TLA+ are handy for proving properties about interesting systems. The latter, for example, sees use for verifying concurrent/distributed systems, which I think can be reasonably described as more than "small and unimpressive"

You can formally prove the correctness of even massive programs.

Not true at all! Most of the HTTP APIs, and a good chunk of the webapps, that I've worked on can be defined as a combination of an API spec that carves out valid and invalid behaviors, and a set of behavioral tests for the workflows that the client users care about. Working from a codebase which is generated from a spec document (e.g. OpenAPI or gRPC) and use of tools like https://pkg.go.dev/net/http/httptest and https://bun.com/docs/test/dom makes this a pretty achievable goal in practice.