Unfortunately, this is extremely unlikely.
It is nearly impossible to make statements about the behaviour of software in general. This is due to the Halting problem, which shows that it is impossible to prove whether a program will stop for any given input. From this result, many other things have been shown to be unprovable.
The question whether a piece of code is friendly, can very likely be reduced to a variant of the halting problem.
An AI that operates in the real world, which is a requirement for "friendliness" to have a meaning, would need to be Turing complete. Input from the real world cannot be reliably interpreted using regular or context-free languages.
Proofs of correctness work for small code snippets, with clearly defined inputs and outputs. They show that an algorithm produces the mathematically right output, given the right input.
But these are about situations that can be defined with mathematical rigour.
"Friendliness" isn't a rigidly defined concept, which already makes it difficult to prove anything about it. On top of that, "friendliness" is about how the AI relates to the real world, which is an environment whose input to the AI is highly unpredictable.
The best we can hope for, is that an AI can be programmed to have safeguards, and that the code will raise warning flags if unethical behaviour becomes likely - that AI's are programmed defensively.