[jaykru]

There's tons of formal verification work available in the hardware industry. Besides that, there's work in defense and AWS has been hiring lots of formal methods people in the past few years. I'm currently working in the hardware industry on formal verification of CPU microarchitecture.

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.

[petermonsson]

Piggybacking on this post:

If you want to go into the HW/semiconductor industry you will be looking for the job title Formal Verification Engineer.

Pay is not as good as the SW industry, but still good.

Demand as jaykru says is exceptional.