Job search in AI + FV/compilers #7 — weeks 5 & 6 I am VERY happy to announce that the job search is officially over! I’m joining the Beneficial AI Foundation (BAIF) as a Research Engineer, working on formalizations of Rust in Lean and other exciting problems at the intersection of formal verification and AI safety. Honestly, this feels like an incredibly good match for me. The role combines theorem proving, programming languages, real software, and one of the questions that has motivated this entire series: as AI writes more of our software, how do we obtain strong evidence that the resulting systems actually do what we intend? I’m also extremely aligned with the mission, culture, and leadership behind BAIF. The more I learned about Max Tegmark’s work and BAIF’s mission to keep AI beneficial for humanity, the more excited I became about contributing to it. I would especially like to thank Shaowei Lin for believing in me and in my work. I’m very excited to see what we’ll build together! Now, as a postscript to this job search, here are some numbers. I applied to 47 companies in total. That number could have been much larger, but I deliberately focused on strong matches: places where my background was relevant and where I genuinely believed I could be happy doing the work. Of those 47 companies, 15 invited me to interview. Across those processes: • 7 ended after one round • 3 reached two rounds • 2 reached three rounds • 1 reached four rounds • 1 startup invited me to a three-week paid work trial • 1 ended with the offer I accepted from BAIF 🎉 The work trial was particularly interesting. The startup was very transparent from the beginning: they explained what they wanted to evaluate, how the trial would work, and even what the offer would be if we decided we were a good match. I appreciated that a lot. Hiring is an exhausting and resource-intensive process for BOTH sides. Candidates invest time, energy, hope, preparation, and often a slightly unreasonable number of LeetCode mornings. Companies invest the time of recruiters, engineers, researchers, and leadership. So I want to thank everyone who interviewed me for their time and patience—even when the answer was no, or when the process simply showed that the match wasn’t right. And thank you to everyone who helped me along the way. A lot of people reached out with advice, introduced me to companies, invited me to interview, shared my posts, or simply wanted to connect. I think I made some real friends during this process, which was one of the best and most unexpected parts of the whole thing. I also want to leave something useful behind for the next person searching. During this process, I tracked companies hiring in formal verification. I’ve now turned that work into FVjobs, a public job board for roles involving proof assistants, automated reasoning, verified compilation, hardware verification, and AI-for-proof: github.com/typetheoryforall/… I plan to keep maintaining it, but I would love for this to become a community resource. If you find an open formal-verification role, you can submit it through a short GitHub form—no Git knowledge required: github.com/typetheoryforall/… Pull requests are also very welcome! Formal verification has received an incredible amount of attention recently. I want to help turn some of that attention into connections between the people who need these skills and the people who have spent years developing them. For the last several weeks, I’ve been writing publicly about the uncertainty, interviews, mistakes, preparation, and occasional moments of hope that came with this search. And now I can end it on a high note and giving something back to the community! Thank you to everyone who followed along and rooted for me. I can’t wait to get started!