[Jweb_Guru]

Do you believe that "just applying TLA+ to the rendering code in Firefox" is a useful thing to recommend to people? TLA+ cannot scale to that size of a codebase without such dramatic simplifications that it's not going to catch any of these kinds of bugs. This is the entire reason why proving safe encapsulation of `unsafe` blocks is possible was so important, it lets you focus the proof engineering effort on a much tinier part of the program. Sure, it can't prove the kind of global invariants TLA+ aims for, but you can also actually apply it to a very large codebase like Firefox (and keep it in sync--another problem you need to deal with when using tools like TLA+).