I agree; I would say that most can be taught to people without advanced math/logic degrees/backgrounds, but because the tools are created by (and usually for) people with formal verification majors), they are just quite bad ergonomically as you say. I think we are in a good place of making it these types of proofs easier and faster more mainstream effort, not just one professor and their students, is put behind it. I believe AI will play a part here.