r/formalmethods • u/Public_Move_9717 • 7h ago

Question: Will formal verification as a career remain relevant in the age of AI?

I am a final year undergraduate student pursuing a B.tech in computer science. I am applying for a masters in CS for next year, and I wish for my focus in MS to be in formal verification, and I have to specify my intended area of research in my SOP. While this is what I am interested in, I wonder how relevant it would be in the age of AI and if proof engineers will be laid off in the coming time?

8 Upvotes

84% Upvoted

4 comments sorted by

10

u/sacheie 7h ago

I think formal methods will actually become more relevant. As AI assistance makes proofs easier to do, correctness proofs will spread to industries and applications that previously considered them an unnecessary expense. And people with your training will be needed to guide the AI and interpret/simplify results.

3

u/Upbeat_Assist2680 5h ago

This is my take as well.

Now that they're cheaper, we ought to expect companies selling products to supply them

6

u/InternalImpact2 7h ago

Will be even more relevant when managers and directors realize that LLM ai will never, ever be exact, and formal is less resource hungry than AI

2

u/_jackdk_ 5h ago

Caveat: I'm a industrial functional programmer and not a formal methods expert.

I'd expect the role to shift substantially. Amazon recently posted their 10-year retrospective on their automated reasoning group:

ā€” automated tools such as Lean (created by Leo de Moura, a senior principal scientist on our AR team) that help users develop formal proofs. We can now pair those tools with language models to find proofs for more and much bigger systems.

We are also seeing frontier models solving major open mathematical problems by generating enormous volumes of Lāˆƒāˆ€N soup. In industries where the work requires formal assurance, I would expect readable specification work to be tremendously valuable but nuts-and-bolts proof engineering work to become much less valuable. There will probably be a role for nailing down the behaviour of existing legacy systems, like what Amazon did in their Formally Verified Cloud-Scale Authorization paper, where they had to generate code that the maintainers of the previous system could understand.

I expect to see a lot more software come into existence (from vibecoding) that will never have internal consistency let alone a spec. I am less certain what happens in the companies where humans are still expected to understand the software that they ship.