" But that is, AFAIK, not what is normally meant by "lightweight formal methods" (although I am not sure there is a very precise, well-accepted definition). "
There isn't. The general usage in CompSci for that is notations that beginners can learn easily, apply with minimal effort, and get results with. TLA+ model-checker knocking out hard-to-test errors in protocols without having long process of formal verification qualifies it. SPIN was popular before it for a lot of similar stuff. Alloy is another commonly called lightweight in the literature with lots of resources for learning. Abstract, State Machines (ASM's) was another one engineers picked up super-easy that caught problems in all sorts of application areas. I think the consensus is the training time has to be tiny, the method should be applicable without a paid specialist constantly helping, and the method should work on useful software with not much extra cost. I say useful rather than practical because some lightweight methods are just shown to work better on academic examples than full formal whereas others were used in actually solving practical problems. There's often overlap, though, where small problems former handles indicates they might shake problems out of a component in a real project which sometimes happens.
"Model checking is the most common form of full formal verification. It is true that because most TLA+ specifications -- unlike most software that's verified with model checkers -- has an infinite state space and that TLC, the model checker that's packaged with the TLA+ toolbox is an explicit state exploration model-checker with not support for infinite state spaces, then most of the time it is used on a finite-state derived specification and so doesn't fully verify the spec."
You just contradicted your own point (and mine) there. The model checkers usually only do partial verification due to state explosion. "Full, formal verification" shows the property applies in all executions typically using some logical methods. The model-checkers are therefore not full, formal verification because they don't cover all states. They're partial verification that gets one some assurances with minimal effort vs full, formal verification that aims for max assurance at high effort.
The combo of ease of use with finite-space, model checking makes that form of TLA+ a lightweight, formal method. One could certainly use it for heavyweight stuff with proving techniques. Most won't, though. That's why my generic comments on TLA+ are about model-checking. I still will be more specific in future.
"They are not aimed at industrial use at all. I know that the people behind Lean -- all accomplished experts in formal mathematics -- have made some claims about its suitability for verifying software, but AFAIK, none of them has any practical experience in software verification in industry, and so I find their claims to be entirely hypothetical."
I was saying it was designed for verifying programs/systems which you said it was not. You contradicted the authors' own claim about its purpose. I corrected that. I don't follow Lean closely enough to have been making any broader claim past what their intention was. Coq and the HOL's are used in industry for high-assurance systems. I guess whether your claim about them is true depends on what the definition of "aiming for industrial use is." Others used in industry in past or present include ACL2, Z, and B method.
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. They surely aren't putting a lot of effort into making the tools easy to apply in industry like we saw in TLA+. That's not their priority. They do get used, though, so not useless for that. Just needs costly specialists. So, they are tools with industrial application that have gotten excellent results in quality/security delivered that are just hard and expensive to apply with a need for specialists. There's a lot of things in industry that work like that where average person you pull out of college can't replace the expensive specialist. We don't usually pretend in those cases whatever the specialist is doing isn't fit for industry. We just recommend or use it very carefully while minimizing a need for it.
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. Also, doing one or both until there's an ecosystem of reusable, verified pieces that can be composed for future projects like concept of Verified Software Repository or how so much is building on CompCert's Clight. One of only ones with industrial focus was SPARK Ada. There's a world of difference between effort involved for a newcomer to learn and use that versus Coq for a similar program even they were gonna try to run the Coq stuff through an automated prover. Like TLA+, SPARK was designed and improved by engineers for other engineers being tested regularly by use in engineering projects. I agree with you that the field needs a lot more of that thinking and investment into delivering it.