I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps i

I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps it's writing the automation that is hard right now due to a small overlap in skills. Writing the proofs is one thing but writing the automation that scales those proofs to a larger system and which makes it easy to extend the system without breaking the proofs constantly is key and requires more "engineering" focused people rather than proof-focused ones.