> I’m not aware of apprenticeship models. Maybe not a popular answer, but I think the answer to this is grad school. Someone gets a PhD in an area like this (e

> I’m not aware of apprenticeship models. Maybe not a popular answer, but I think the answer to this is grad school. Someone gets a PhD in an area like this (e.g., building either theorem provers or their related infrastructure), then gets a job in the same or an adjacent area after graduation. That's not the only way to do it, but looking around in my area of research (compilers and programming languages for HPC) there are definitely many more people who do it this way than just figure it out on their own.