How is getting proof one doesn't understand going to help build safer system?

I want to believe formal methods can help, not because one doesn't have to think about it, but because the time freed from writing code can be spent on thinking on systems, architecture and proofs.

That's a fair question, and looking at my post I now realize I have two independent points:

1. A proof mindset is really hard to learn.

2. Writing theorem definitions can be hard, but writing a proof can be even harder. So, if you could write just the definitions, and let an LLM handle all the tactics and steps, you could use more advanced techniques than just a SAT solver.

So I guess LLMs only marginally help with (1), but they could potentially be a big help for (2), especially with more tedious steps. It would also allow one to use first order logic, and not just propositional logic (or dependant types if you're into that).