Even that is getting automation as I long ago predicted. I think the SPARK-type proofs will be easier to automate this way, too, since they're more mechanical.

https://blog.acolyer.org/2019/08/23/learning-to-prove-theore...