I've seen a video intro [0] and poked a little bit around the reference manual [1], but I'm not sure what's "between" basic understanding of the commands and being able to extract a complex verified program.
It all seems to be either the theory (which I mostly grok) or completed projects, not a lot about the engineering details.
...Or does that just not exist?
There's also an annual summer school on the topic which has downloadable videos available: https://www.cs.uoregon.edu/research/summerschool/summer17/
The DeepSpec summer school, however, did lead with a Coq intensive, which was recorded and included in the uploads at https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw .
Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial.
TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.
Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.
[1] softwarefoundations.cis.upenn.edu/current/index.html
(And for a bit more about Coq to Rust, Program extraction from Coq https://github.com/rust-lang/rfcs/issues/667 )
[1] https://www.manning.com/books/type-driven-development-with-i...