The Coq mailing list

[Alyssa N Byrnes <abyrnes1 AT cs.unc.edu>]

I know Intel also has a formal methods group. Also, some major car companies are now looking into it!

Alyssa Byrnes 

On Jan 26, 2023, at 7:09 AM, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:



Hi Kevin,

Theorem proving skill is very valuable in areas where stakes are very high. For example, recently many cryptocurrency companies are looking for experts in formal verification to ensure their funds are secure (Certora does smart contract auditing using formal methods, Veridise works on blockchain security, Runtime Verification is also in this domain but they do some cool stuffs as well, Formal Land uses Coq to write secure smart contracts, and there will be many others). Cryptography is another domain where you need correctness, and Cryspen is one such company that is hiring for formal verification experts (maybe Adam Chlipala, Karthikeyan Bhargwan has more to say on this). Amazon has a formal verification group that works on securing their internal infrastructure. Galois is another company that hires formal verification experts. 

Also, given that theorem proving is just functional programming, at least that’s how I see it when I write Coq proofs/programs, you can apply the skills learned in theorem proving to any other job involving Haskell, OCaml, Scala, etc. Hope it helps. 

Best,

Mukesh

On Thu, 26 Jan 2023 at 04:37, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

Suppose an undergraduate or MS student gets entranced by Cow, Lean, formalizing math, etc. But they do also ask, "For what jobs at what places might I reasonably expect to be prepared by virtue of having learned logic, languages, reasoning, and maths stuff?" An appeal to anyone who might add an entry here, in response. Thank you in advance. --Kevin Sullivan, UVA CS