Ask HN: Career in Formal Verification | Hacker News Reader

Ask HN: Career in Formal Verification

6 pointsdir_balak7 comments

I am currently in academia as a postdoc in math and I'm on the lookout for opportunities in industry. I stumbled upon the field of formal verification which seems particularly well suited for someone with a deep math background and sounds definitely interesting. My knowledge is very superficial and I would like to know better this niche and the thoughts of industry professionals on it. Some of my questions: - how interesting/stimulating is the work? - what is a typical salary for a formal verification engineer? - how do you value this field? Is it going to grow in the coming years? Is there demand for these roles?

View on HN

In addition to for-profit companies, some non-profit research organizations and government agencies do formal verification research work. I encountered with some researchers from Formal Methods community over 15 years ago. Those folks worked for and with NASA, SRI International and Mitre Corporation.

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.

There are a few consulting companies that specialize in this. For example Galois [1], with offices in several US cities. In the UK there is (or was) Praxis [2]. (I have never worked with either, I have just heard of them).

1. https://galois.com/

2. https://en.wikipedia.org/wiki/Altran_Praxis

how interesting/stimulating is the work?

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.

Hillel Wayne seems to be doing something like this. You might also look at Gerard Holzmann's career.

https://en.wikipedia.org/wiki/Gerard_J._Holzmann

Do such things really happen at enough scale and regularly for a company to pay a salary for it? (Note: I'm not asking if they should!) This stuff is hard and the size of entities that can be specified and verified this way is going to be tiny compared to typical deliverables outside very specialist niches I guess.

(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!)

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.

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.

Reply on news.ycombinator.com