[calf]

Formal proof is problematic because English has no formal specification. Some people are working on this, it's a nascent area bringing formal methods (model checking) to neural network models of computation. But it's an interesting fundamental issue that arises there, if you can't even specify the design intentions then how do you prove anything about it.