Usefulness of formal verification (Coq) and formal specification (TLA+)?

I'm curious about formal verification courses like Software Foundations[0] (specifically volume 1 & 2). I'm also curious about formal specification with TLA+[1], which seems less academic-oriented and more relevant to my career pursuits in software dev.

I'll get around to delving into both of these topics eventually just for fun, but I'd like to know what HN thinks of its usefulness beyond intellectual curiosity. I don't remember where, but I've read online comments claiming that TLA+ can really change and improve the way one thinks about software design, and that it's made to be used in regular dev jobs. And I bet there's something to gain from learning how to use Coq, even if I never use it in my day job.

I know this will cause some eyerolls, but I do wonder how this will all fit into a future way of software dev where most of the code is written by AI based on simple pseudocode, as the next form of "high level" programming. There was an interesting discussion about this [2] a few days ago.

[0] https://softwarefoundations.cis.upenn.edu [1] https://lamport.azurewebsites.net/tla/tla.html [2] https://news.ycombinator.com/item?id=39934956