[0]: https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ [2]: https://leanprover.github.io/
IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input.
The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency.
You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work.
[1] https://github.com/seL4/l4v
[2] https://www.idris-lang.org/
[3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht...
Everything starts with two logic courses EECS/MATH 1028 which covers basics like induction and pigeon hole princele and MATH 1090 which covers first principles and axioms of logic.
Then, using the courses on logic that we did by hand, we have a system verification course (EECS 3342) with SMTs like Rodin which can solve on its up to a point where we need to manually input the proofs. Beyond this, we also cover proving preconditions and post conditions through design by contract in EECS 3311 - Software Design (which is usually tough in Eiffel, but finally being taught in Java after a year of lobbying the faculty).
Then our final courses are EECS 4312 and 4315 for requirements engineering and mission critical systems respectively. In 4312 we learn TLA+ and 4315 is focussed on tree and path logic for states. As well, we have EECS 4313 advanced software testing which is primarily about writing bug reports, creating tests (JUnit) and touches on distributed systems tests a bit.
The point is that we do learn the "practical" (quite impractical since our prof's are not in industry) only once we have had a lot of exposure to proving things by hand. But even once we have learned everything, they fail to connect material to realistic SDLCs and how to implement the tools in an agile methodology.
Viewing college as a trade school is a mistake many of us make. No, you're almost certainly never going to be manually proving things by induction in the real world. But that doesn't make the exercise valueless.