In terms of how to get those roles, these folks worked on topics related to Formal Methods during their graduate studies. They got the positions from the connections. Those jobs could be niche. They weren't widely advertised like an SWE for a software company. Those organizations could be conservative and moving in a much slower pace than Silicon Valley software companies.
Some individuals stayed in those organizations for a long time. Depending on your nationality, working in those US organizations could be tough. The one worked for NASA left due to a policy change in the hiring policy for non-US citizens: They weren't an American. Despite the abrupt departure, they still joked from time to time that they worked for NASA.
Subjective.
what is a typical salary for a formal verification engineer?
It will depend on the application field. At a minimum I could see three potential fields: provable security (OS level eg. SEL4, application level, distributed system level TLA+, etc.), analysis (reversing/verification of compiled artifacts), and specification (industrial control and safety systems).
how do you value this field?
I don't see it a specific field at all. More like a group of approaches. Clearly they are most valuable when there is an end-user / application domain requirement for extreme clarity. This is usually associated with high cost development and assets such as aerospace, industrial, military, nuclear, space.
Is it going to grow in the coming years?
Can't crystal ball but I believe there is untapped potential for formal specification and resulting verification in the industrial space, particularly as reshoring of automation-heavy production accelerates.
Is there demand for these roles?
If you'd enjoy the industrial stuff, shoot me an email and I will introduce you to a founder I've been advising in the space.
(Disclaimer: decades ago I raised seed investment from a major engineering firm to do some of this stuff, and I think that I proved to myself that getting beyond a toy was implausible. I have a licence for the Edinburgh Concurrency Workbench that I can sell you!)
To answer your questions:
- It's sort of a crapshoot from what I can tell. I'm early in my career and working on an early stage from-mostly-scratch CPU project, so your mileage may vary. Some of the work can be really stimulating--modern CPU designs are very intricate and just understanding the design well enough to formally specify its correctness can be quite fun. Frequently the problems will be fairly routine and your effort will be spent slogging through bugs in junky vendor tools. One thing to note is that the economics of formal verification in industry are quite different from academia. Timelines are short, and getting a partial proof of correctness with a quick fully automated method (e.g. model checking) is greatly preferred to a full proof of correctness with manual reasoning in a tool like Coq/Isabelle/Lean, which makes the work way less appealing from a mathematician's perspective.
- The salaries don't seem to come close to top of market for FAANG software engineers, but it's comparable with tier 2 software companies. I have heard Qualcomm especially and Apple pay close to FAANG top-of-market for formal verification engineers. My starting total compensation out of college with 1YOE between college years was about $165k, which is $22k less than what Google pays new grads according to levels.fyi. With a post-doc, you could start much higher, I would guess. AWS would pay well, of course. Hardware startups might also pay better.
- Going to answer the remaining 3 in one go. This is a super cool field with a rich academic literature to pore over, but it's held back by immature tools and a very conservative culture in the hardware industry. I think the growth and maturation of the field over the next few years will be very exciting, especially as recent developments in AI/ML are brought to bear on formal methods. There's exceptional demand for formal methods engineers in the hardware industry. From what I can tell, it is very difficult to hire for these roles, and they are generally filled internally by people with a conventional validation or digital design background who want to try something new. You won't be competing with many people for job postings.