Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Jobs for undergrads / MS students with proof chops

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Jobs for undergrads / MS students with proof chops


Chronological Thread 
  • From: Alexander Gryzlov <alex.gryzlov AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Jobs for undergrads / MS students with proof chops
  • Date: Thu, 26 Jan 2023 14:14:09 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alex.gryzlov AT gmail.com; spf=Pass smtp.mailfrom=alex.gryzlov AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f175.google.com
  • Ironport-data: A9a23:NocICK0jSb5sPy78U/bD5QB1kn2cJEfYwER7XKvMYLTBsI5bp2RWn 2dJC2qBO/3fZDb3e94gPo7l9EMCv5fczd9mHQs+3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOH9IQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3ZRn0hFaYDkpOs/jY8Eo14qyp0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJWyXmxdlXBk4pAYRb1OZbBnBK+ 8U8OS9YO3hvh8ruqF66Yuxlh8BmPdayeY1G5SwmwjbeAvIrB5vERs0m5/cChGZ21p0IRKyOI ZNGNFKDbzyYC/FLEl4TBYJ4k/25lH34bRVXrVuUoew85G27IAlZjOa1YICIJ4ziqcN9kWuqv jqc80XFCC4ECdG57zml2XSBr7qa9c/8cNtKSOfQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vC8jiBli2+SHZ+BEbXNVUHqsx7wTlJrfoDxixWGICYgdLZ8MavYwYRRAtx 1uHpvf4Gmk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz8OnfaTqfHr5e/L6JYs7dQm6vn mjbxMQqr/BC0p5RjvTTEUXv2mr0/vD0ohgJChI7t19JAyt8bY+hIp23sB3VtKkdaomeSVaFs T4PnM32AAEy4XOly33lrAYlRunBCxO53Nv03wUH834JqW7FxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzuV5p1lPS6S4q5DZg4i+aihLAhJGdrGwk+NSatM5zFzSDAbIlla MnGLpn8ZZrkIfs3kmPeqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchgtPnsiFyNr b53bpLWoz0CDrCWSnSIqeY7cwpWRVBlXsueg5IMJoa+zv9OQj5J5wn5muN/JeSIXs19yo/1w 51KchYJlgSg3C2bc1jih7IKQOqHYKuTZEkTZUQEVWtEEVB6CWp2xPZFKckEbvM8+fZ9zPV5a fAAdo/SSr5MUznLsXBVJ5X0sIUoJlzhiBOsLhiVRmE1X6dhYAjVpf7iXA/krxcVAgSN6MARn ryH1yHge6QleThMNsjtRcyK80KQplkYweJ7YFvJKIJceWLq64lbFBbyhf4WfeAJcBXK+SSG2 jadETMnlPnrsbIowoOYm5Lev4ONFs1gFHF7BEje1669bgPBz1qgwKhBceeGRi/cX2XK45efZ f1Z4vX/Ef8flnNIjtZMKKlqxqcA+Nffnb9W4QB6FnHtbV7wKLdfDlSZ/MtI7Ith+6R4vFaoZ 0ex5dVqA7WFF8f7Glo3JgB+TOCi1+kRqwbC/8YOP0T2yy9mzoWpCXwIEUG3txVcC79pPKcO4 +Qr4pcW4jPirCsaCI+NiyQM+lmcKnAFbb4ciagbJ43V2y4L0VBJZKLOBhDmuK+vb8p+CWh0A zu2qpebuZFi6BvsT34BG0LJ/9JhvrUVmRUTzFY9N1WDwdXEofks3Sxuyzc8TyUL7xBLz9NMP nNPMmtrL56v5BZtvtBIBEq3KjFCBTqY203/8EQIn2vnVHuVVnTBAWk+GOSV9mUbzj54Uh1E2 oqHkUDJfC3Pfs7j+gcTA2tetO3FX9h90ibgifKXNZ2JMLdiaAW0n5L0Q3QDriXWJP8YhWrFg LJP1/lxY6iqDhwgifQ3JKfC3ItBVS3eAnJJRMxg26Y7HWv8XjWW8hrWImCTfvJ9HdD7wXWaO edPeP0WDw+f0RyQpA81HaQPer94vMA47eo4J4/EGzQ0jKu9nBFI7rTgrjPzlU06ceVIyMwdE L7cRxiGM26XhEZXpVPzkdl5CjK4TOQANSLB37GT0eQWFpg8nvlmXmMs35CV4XiEEgtV0CiFn QHEZp2Mluxr9ptxrtG9DoRCGASGBtfhX8uY8A2IkopvbPGeFezspg8qul3cEAAOBoQoWvNzj qWrjNHs+VHs5ZIabjj8oIaQMIVs/uCwbfpzHuOsC0cChgqEesvnwyVbylCCMZYTze9svJi2d TW3eO6bVIAwSdxC4FZ3diIHMRIWK5qvX5favSnn8si9UEkM4zfmcuGi22TiN1xAVykyPJb7N A/4ltCu6v1cr6VOHBU0PO5nMbApPG7cXbYaSPOpuQm6FmWIhnawionmnzck6hDJDSCKLp+rq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ/0RY5L3f2N0uUyTbCiyCcWLB74JGuKMJZtpUmOL8Q1lA Yh2Fr7M0tyZzZRgROJV7fu+6Qui7u2P3WoGoCgRjOSrayvzwtw2OLhJEw9EVCiBGMbI/KkOy a7ZWkgcKHyGpYXN/QqMtpKb9Nz1fN8i8tnwURqy/Q==
  • Ironport-hdrordr: A9a23:Bwe9rKt/OZ9Q5iHMeg/fs4yS7skDT9V00zEX/kB9WHVpm62j5r mTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U 4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
  • Ironport-phdr: A9a23:TjMbMBD6rZdWh2n4C+jjUyQUlUkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygaTAc6HtLptsKn/jePJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYwhEniexba19I Rm5ogjctNQdjJd/JKo21hbGrXxEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2V KRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+4 6t3ThLjlSEKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xa ZYEAeobPeZfqonwv0cDrR+gCgijHuzvzCJHiWHs3aYn0uohCwHH3Q0kH9IJrnTfsdL4O70WU e+rw6jE1zrDb+lW2Db87IjIdQ4hrOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkCvGaH9eRvT /6vi3I5pAFrpDii3sgih4vXio8ayV3J9yt3zZorKNCmTEN2YdGpHZtNuyyeN4V7Rs0sTm9pt Som1rALupC2cSoUxJk6xRPSavOKfYaO7xn+WuiRJjJ4i2hkeLK5nxuy/kmgyvH8Vsmpy1lGt DZKkt7Jtn0Lyhfd6dCHR+Nj8ku93TuDzQPe5+FeLUwpi6bWKIQtzqMym5cTt0nIAzX4l1/sj KCMc0Up4uio5PrjYrXhvpKcMpV7igD6Mqg3ms2+D/k0PhEAX2SG++mx1Kfv/UL+QLVNgf02l rfWvIrGKsQco661Gw5V0oA95BajFzqqzsgUkH0dIF9GeB+LlZXlN0/NLfziEPuygVShnC9ux //cP73hBpvNLmLEkLfkZbty8UpcxxQ8zNxF6JJUELEAIfP3Wk/2qtzVFRA5MwmuzObmDNVxz J8RWWWKAqOBNqPdqkeH5vgzLOmUeI8VpDH9JuA46/L2l382hUcdfbW13ZsQcH23AvNmI1yAb XXwhtcBDHwFsxElTO3qjV2CSSRca2yzX6I6/DE7CZipAZ3NRoC30/S923KwGYQTbWRbAHiNF 23pfsOKQaQiciWXd+ZlnywNU7SsUccOzwC8sAjkg+5uKufEvCICpIDn08Zd6OjalBV0/jtxW ZfOm1qRRn15yztbDwQ927py9BQVIjar1KF5h6cdDtlP/7ZSVR98M5fAzut8AtS0WwTbf97PR kz1Cs6+D2QXSdQ8i8QLf147A8+r2xnH0jrsDKUEhbiMGrQ796vd2z76IMMug23e2vwZhkI9C tBKKXXgg6d+8wbJAIucmkGUh+Clb7UO2CnT3GiGxGuK+kpfVV04Sr3LCFYYYEaettHl/gXCQ rupXKwgKRdEwNWeJ7Fib9ToiRBXW66mNo2BPiS+nGC/ARvOzbSJBGbzU0Ma2iiVSE0NkgRIu G2DKRB7HSC55WTXED1pE1vrJULq6+h37n2hHAcyyEmRYktt2qDQmFZdjOGAS/4VwrMPuTsw4 zRyElGn2tvKCt2G7wN/daRYaNk57R9Jz2Xc/wB6O5WhKehliDt8O0x+u07+kRptG5dEltYCo 3YjzQ40IqWdkRtAez6ewZHsK+jPMGChmXLnI6XS21zYzJOX4vJVsKV++wil5Vv5UBN9riYCs ZEdyXaX65TUARBHVJvwVh1y7B1mv/TBZTF74YrI1HpqOK3ysznY2ttvCvF2r3ToN9pZLq6AE xf/VsMAAM37YuUulkjvYQgVLuRV6oY7Osqnc72N36vhb4MC1Hq2yH9K5oxwyBfG/i5xWqjHx YcXx/aG9gSCXjb4ylymt4qk/OIMLSFXFW25xy/+AYdXbaAnZocHB1ClJMivz8l/jZrgM5JB3 GaqHEhOmMqgeB7JKkf4wRUVzkMP53quhSq/yTVw1TAvtKuWmiLUkazucx8OO2gDQ2cH7x+kK Iy5n5YVRlm6aw83vBSg7Ef+gaNcoexzInLSTkFBYyXtZzs6A+3g6/zbOZ4Jscx1+SxMGPyxe 1WbVqLwr354m2v4Em1SySp6PzCmt5PlngBr3WeULXJ9tn3cKol7wRbS4sCZROYEhGJXAnklz 2CNVh7lYIT6mLfc343Oue2/SW+7A5hacC2wiJiFqDP+/mpyRxu2g/G0nNTjVwk8yy7ykddwB kCq5F7xZJfm06OiPKdpZE5tURX178dqXI5kg5k0g4841n0Th5HT9n0C2zSWU50TyeflYXwBS CReidfR7Rij11dyPHaO2ar2U3ycxo1qYNzwMQZ0kmotqstNDqmT9rlNmyB490G5oQzmav94h j4ByPEq5S1Sk6QTtQEq1CnYHqEKEBwSI3n3jxrRpYPbzu0fdCO1fLO3zkY7gd2xEOTIvFRHQ HigMpY6QX0rs4MmYQqKiiGsrNmjIoWYbMpP5EPI1U2b1K4Mdsp3zr1T1E8FcSr8pSF3lbB91 EQ0m8n85M/dcy1s5P7rXEAebGGkIZNLvGmq1/4Wn97Kjd/1WMw9XGxaBt2wCqv4dVBa/fX/a 1TRTHtl8CrdQfyHWlbBoEZ+8yCWS8Dtbi7IYilflZI4HVGcPBAN2V9PGmxrwthhUFjtnZKEE g8x5yhNtASg+10cl6QxbUm5CiCG+0+pcmtmEsHBakcGqFgTvQGNdpXPpuNrQ3MCp8Pn9lfcb DfBIVwPVDBsOATMEVnnOvPGCcDo1e+eC6L+KvLPZe7LsulCT7KTworp1IJ6/jGKP8HJP394D vR91FARFXZ+U9/UnTkCUUl132rEctKbqRGg+yZ2stH38fLlXxjq7JeODL0aOMtm+hS/i6OOf +CKgyMxJTFd35IKjXjGrdpXlEYVkD1rfiKxHK4osCfMSOfBhfYSAUdENmV8M8xH66961Q5Ie Ibaht7zyr9kn6s1BlNCBjmD0omiYc0HJX34NUuSXh7acuTbY2SRk4euPv7vLN8YxP9ZvBCxp zuBRkrqPzDY0iLsSwjqKuZUyieSIB1Zvoi5NBdrE2nqCtz8OXjZeJd6iyM7xbosizbEL2kZZ HJ1d05d6LKK/DFchetXFGlI734jJu6B0XX8jaGQOtMNvP1nDz4h3fpd+2g/wqBJ4TtsQfV0n G7DsYcrrQj5z6+AzT1oVBcIoTFOztHu3w0qKeDS8Z9OXmzB9RQG4DCLChgEkNBiD8Xmp6Faz tWnfE3bJzJL8taS9swZVZG8wCOvNXMgNV/4B2eRAlJaEHikMmbQg0Ebm/aXpCX9Rn0SpZ3lm Z5IQbheBgRdKw==
  • Ironport-sdr: 63d27d3a_NzzxIa5ZE4aSsht2HqPUwZ1wOCE40my/P4k4ksfzKpRZq2h 4Cl5VRFez8BYoopbjohp3OOzINcr4V7SlSLI9qw==

There's a community-curated list of companies that use formal methods in some capacity: https://github.com/ligurio/practical-fm/. Seems to be fairly up-to-date but could always use some updates if you have them.

Alex

On Thu, Jan 26, 2023 at 1:16 PM Alyssa N Byrnes <abyrnes1 AT cs.unc.edu> wrote:
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



Archive powered by MHonArc 2.6.19+.

Top of Page