How does one learn and get involved with formal verification outside academia? What sort of mathematical background is required.

I always get lost with pure functional languages and the related subjects, even in the introductory material. Though I’ve been able to understand the usefulness of both some functional concepts (through playing with various impure languages like F# or Erlang) and of formal verification (from looking at SPARK with Ada) but all the notation and vocabulary and such of languages like Isabelle’s HOL and Idris confuse me. I even find myself lost among Scala developers.

a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to": i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable ii) some bit hacks compute the same thing as the non-hacked implementation

b) "use TLA+[1] to verify concurrent stuff with race conditions": i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm) ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used

2) For doing it more for fun than short-term gains: a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI}) b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL. Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case.

[0]: https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html [3]: [edit: apparently it is neither IRC nor Matrix, but rather Zulip:] https://isabelle.zulipchat.com/