Roadmap to formal verification
My goal is to be able to judge what parts of formal verification I
  could apply to my job as a software/network engineer.


If you plan to use formal verification as black boxes, then I would suggest using some tools to have an idea how they work. Here are some open source tools:


Error Prone of Google
Nullaway of Uber
Facebook Infer
Ikos of NASA
Java PathFinder developed by NASA, now maintained by community.
Clang Static Analyzer of Apple
...


If you want to understand their basics, you can start with the book "Principal of Program Analysis". It covers many basic topics from Type Theory to Abstract Interpretation etc. 

The book doesn't discuss anything deeply. For example, it doesn't discuss any abstract domains, the key part in abstract interpretation. Recent topics such as separation logic, which Facebook Infer is based on, are not covered either.

If you want to learn advanced topics, the only way is to read the proceedings of top conferences, e.g. POPL, PLDI, CAV, VMCAI, SAS, ICSE, FSE, ASE, ISSTA, etc etc.



A comment by @DmitriChubarov


  As I understand this is a question of why there is so little use of
  formal methods in the practice software development, ... or is there?


There are companies that are earning hundreds of millions a quarter by selling static analysis tools (I work for one of them), so I believe the number of companies that use formal verification is not little at all.