> TLA+ model-checker knocking out hard-to-test errors in protocols without having long process of formal verification qualifies it.

But that's the mainstream of formal methods. 99% of formal methods in industry is using model checkers or static analyzers. What you call "a long process of formal verification", meaning, I assume, formal manual proofs is almost nonexistent outside academia. So what you call "lightweight" formal methods is normally just called "formal methods". What you call "full" formal methods is, for the moment at least, a research conjecture.

> The model checkers usually only do partial verification due to state explosion.

That's quite inaccurate. To be called a model checker, a model checker must check a model (in the formal logic sense) -- i.e. it must exhaustively search through the entire state space (some model checkers can exhaustively check infinite state spaces), as opposed to, say fuzzers or concolic tests. What happens in practice most of the time TLA+ is that the model checker exhaustively checks a finite-state specification (or a finite-state instance), which is derived (by the user) from an infinite-space one. Model checkers are not "partial verification". They can be used to do partial verification. But so can proofs.

The theoretical difference between model checkers and proofs is that the latter is based on proof theory, while the former is based on model-theory. The challenge for model checkers is trying to automatically cover huge or infinite state-spaces; proofs have the same challenge, but they work manually with the hope that the human prover would be able to assist (this can actually be done with model-checkers as well, using refinements in TLA+, but TLC specifically is not that sophisticated). This hope is far from realized. In practice, most of the time, proofs hit a limit much sooner than model checkers, which is why they don't scale as well in practice, and so are barely used (when they're used, it's usually to tie together results from model-checkers and/or other automated tools).

> The combo of ease of use with finite-space, model checking makes that form of TLA+ a lightweight, formal method.

Again, virtually all formal methods are like that, except those that are mostly used in academia. Manual formal proofs are not only not used because they are so prohibitively expensive, but because they're simply not needed.

> You contradicted the authors' own claim about its purpose.

That's right. Those authors -- as accomplished as they are in their field -- have no experience in industrial software verification. Their claim is mere conjecture. I don't know how someone is supposed to design a tool to serve a certain market if they've never researched that market. I find Lean to be very interesting (I'm playing with it as a hobby), but its authors make some unsubstantiated claims that are well outside their area of expertise. I remember their introductory paper sometimes says things like "in practice", when it is clear to anyone who's actually done that in practice that, at best, they could say "in theory".

I should, however, qualify that Lean does have some features more oriented towards software verification, like -- most importantly -- integration with SMT solvers (which pretty much amounts to a model checker). But Lean does not differ in that regard from Why3 or Boogie, and I assume that's not the part of Lean you were referring to.

> I'll be the first to agree each has a main goal of being designed by experts in such tools for use by veterans of or experts in such tools.

Those are not just veterans and experts, but mostly academics working on research projects. There has not been a single piece of large or even medium-sized software verified end-to-end (let alone "fully") by anyone, ever, experts, veterans or otherwise. What you call "full" formal verification does not exist in any shape or form outside our hopes and dreams.

I think that the confusion between methods that are now purely research stage and are nowhere near ready for practical adoption, and actual working formal methods, does a lot of harm to formal methods. In general, I see a worrying trend of pure researchers, who have done little or no applied research, let alone actual industry work, presenting their pure research in a way that can be mistaken for "nearly ready for primetime" does a lot of harm for both research and industry. The field of formal methods in particular suffered a research winter (dried up funding) precisely because of such over-promises. Again, no one has ever "fully" verified a complex, large or even medium-sized real-world software, and even small, simplified software has virtually never been "fully" verified end-to-end outside academia. It's fascinating research, but its no more than (pure!) research at this point.

In fact, I know a company that makes a commercial formal verification product (a very sophisticated sound static analyzer) that can also integrate manual proofs in Coq or Isabelle. One of their customers wanted to try writing Coq proofs, and the team -- all formal math academics -- actively tried to dissuade them (I assume they succeeded) from doing that. How? By showing them how it's done.

> That said, I'm definitely one of the people in favor of getting all that stuff or something similar in shape for better industry adoption. Alternatively or in parallel, attempting to stretch user-friendly methods like TLA+, Alloy, or Design-by-Contract to hand-prove whatever properties the others do.

All formal methods designed for practical use are more-or-less user-friendly (or, at least aim to be), or they wouldn't be used by anyone. "All that stuff" as in tools that are actually able to "fully" verify large, complex software cannot be made user friendly as it does not exist at all. I also don't understand what you mean by "stretching" TLA+. I've used TLA+ extensively and have been learning Lean for quite some time, and there is nothing Lean can do when it comes to software verification that TLA+ can't (although, there are different relative strengths). In fact things like refinement or specification/verification of interactive/concurrent/distributed software -- all things that are of great importance in practice -- cannot be easily achieved in Coq/Lean/Isabelle without some serious work of embedding a logic like TLA in them (as, in fact, has been done when specifying/verifying such software). If anything, I would say that out of the box, TLA+ is more powerful than Isabelle/Coq/Lean for a big portion of real-world software (as most of the software people write today is interactive/concurrent/distributed).

Which is why I don't understand in what sense TLA+ is any "lighter" than Coq or Lean. The difference in power between Coq/Lean and TLA+ has nothing to do with software, and everything to do with researching novel logics and formal mathematics.

I think that you are grossly misestimating what has actually been done in CompCert and other similar projects. Even the main author of CompCert readily acknowledges that model checkers scale better. A closer look at what they did would give you a better picture of the true state of affairs.