That's great to hear esp coming from you. You previously had no interest in these things if I recall correctly. There's a lot more to explore than most people think. Gaining more understanding, synthesis, partial/full verification, timing, flow, verified refactoring, parallelism/concurrency, and so on. As he describes, the formal methods might be there to do something for you, maybe just increase your own understanding, or something else. Most writings are strictly on formal, full correctness but field is broader than that.
Far as Stavely, I have the book in hand now. I think you'll find section 12.2 onward to be pretty inspiring. Since he's not in formal verification, he's not as biased in favor of throwing Isabelle and Coq at everything. His assessment of the past and future, at time of writing, is quite pragmatic. It's also still quite inspiring. Next step for anyone that learns Cleanroom to further assess its modern relevance is seeing how well it works with Haskell's typing, a LISP/Scheme, Smalltalk (or Strongtalk), and any language with Design-by-Contract (eg Ada/SPARK or D). I think a mix of semi-formal and formal contracts might emerge if programmer focuses on maximizing productivity and personal understanding over formality and proof. Some things will also just be tested because that might be easier.
Ok, I misremembered. I hear you. I originally got that from Guttman who focused on shredding claims of high-assurance security as much as verification. Others and I did submit a few things on limitations to Lobsters. They were general. I'll resubmit them to Laarc after I dig them up if you're interested. They might find them interesting, too.