Try TLA+ (learntla.com) for concurrency, Alloy Analyzer for structure, and SPARK or Frama-C for code-level stuff. See if you can feed TLA+ or Alloy properties into stuff like SPARK. E-SPARK did that with Event-B. These are the low-hanging fruit for verification vs full build out in Coq or Isabelle. Then, you write checkers for it to apply testing like KLEE, property-based, or fuzz testing.
These will get you close to full verification with less work. Each of the three languages has been used in a lots of CompSci and industrial work. Note that SPIN is similar to TLA+ and you can Google its industrial use for ideas of TLA+ power in concurrency analysis.
These will get you close to full verification with less work. Each of the three languages has been used in a lots of CompSci and industrial work. Note that SPIN is similar to TLA+ and you can Google its industrial use for ideas of TLA+ power in concurrency analysis.