There is formal specification in the large if you count formal mathematics. Mizar's library of formalized mathematics is easily millions of lines if not tens of millions of lines at this point. There are individual formalized mathematics repositories in other languages (Coq and Agda included I think? It's been a while since I looked into that) that run into the hundreds of thousands of lines of code.

So there are pointers as to how to organize formal specs for extremely large projects.

The reason as far as I can tell for why there aren't large software verification projects as opposed to pure formal math is that the cost benefit analysis is wildly out of whack. It makes essentially no business sense to try to formally verify things past several thousand lines. This doesn't seem like a bright line to me though, e.g. that there is a technological inflection point at several thousand lines that prevents further scaling. Again formal mathematics repositories are a counterexample. It's just that because of the high cost of formal verification, there is a business ceiling at the equivalent of man hours willing to be spent somewhere in the vicinity of hundreds of thousands of lines of unverified code to millions of lines of unverified code and you can rapidly exhaust that budget with full formal verification (which can easily account for orders of magnitude increases in time spent).

Ah thanks for the TLAPS repo. I forgot about the library, but even there I'm not seeing a lot of reuse in it. There's some of it, but not a lot. Maybe just because users of TLAPS are far fewer than users of TLC.

Indeed you can choose specific Isabelle tactics in your BY line. In practice I'm not sure I've ever seen it in any TLAPS proof. I've very very briefly played with that functionality and at first glance it seems much more difficult than using Isabelle directly because of the added layer of indirection. If you have one in the wild, I'd love to take a look to learn from.

I definitely agree there is no one way to do things. I've left out all the things that I think TLA+ is fantastic at. I think it's the closest thing to mathematics that can be practically used in industry. Far more so than the rhetoric you usually hear about FP languages, TLA+ is immediately familiar to anyone with a pure mathematics background, both syntactically and semantically. TLA+, unlike something like Agda, also has a fairly straightforward set of semantics and mathematical grounding in its theory. The benefit of writing each spec from scratch allows them to be independently understandable with no need to understand the idiosyncrasies of arcane libraries or frameworks.

But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space (which honestly don't bother me, my TLA+ specs are often exponential or worse wrt model checking time in the size of my constants, but I still get a lot of mileage out of them), but rather the difficulty in even expressing that idea. When I'm confronted with wanting one state to stand in for two I often have to resort to using two separate specs, one with fewer states and then the other being the original spec and then showing my new spec fulfills both. I think the modularity problems mostly stemming from tooling and language choices, but a little bit from theory (although Mizar is also set theory based). For example I don't think I've ever used a 3rd party module in a TLA+ spec I've written. Even trying to express the equivalence between two specs that just use different strings for the same states can be tricky. Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems? Or any other specs someone has written specifying one part of their system? That would be pretty awesome if there was something akin to an NPM repository of all these specs for various algos that you could import into your own spec. The tools for this exist in Mizar. They do not for TLA+.

Turning my attention back to deductive verification rather than the expression part of the equation, more specifically for TLAPS, I'm actually not a fan of the imperative tactics that are found in Coq. But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS. Something where you can mix YOLOing with more hands-on proof building, with tactics, functions, or even just a trace of the constraint search would be great.

I think the idea that you have some limited thousands of line to "spend" is a useful bit of intuition. One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.

For example absence of crashing/abnormal exits is something that is feasible to prove on very large codebases. It's hard to do completely end-to-end (even CompCert's front-end isn't proven), mainly because of the difficulty of fully modeling stuff like filesystems, but can be done for modules spanning hundreds of thousands of lines of code. It is of course a weak property. That the program does something is nowhere near the same thing as doing the correct thing. But it is nonetheless a very useful one.

Absence of SQL injection attacks and CSRF attacks are other examples (can be done either by external analysis or by leveraging language level features), although those feel a bit more like cheating since you basically cleverly restrict the amount of code that "matters."

That would be the closest to an alternative to formal specifications I could suggest. I still think formal specs are lower risk because this still requires coding in certain styles amenable to this static check (or languages that enforce it).