You might be able to verify interesting properties of code that you constructed for the purpose of making verification possible, but you aren't likely to be able to verify interesting properties of arbitrary hostile code like Clippy would have an incentive to produce.
You passed up an opportunity to point to your proposed verification procedure, so at this point I assume you don't have one. Please prove me wrong.
Usually the label FAI seems to refer to AIs which will be 'provably friendly'.
I don't even know what the exact theorem to prove would be. Do you?
Evolution. Morality. Strategy. Security/Cryptography. This hits so many topics of interest, I can't imagine it not being discussed here. Bruce Schneier blogs about his book-in-progress, The Dishonest Minority:
I am somewhat reminded of Robin Hanson's Homo Hypocritus writings from the above, although it is not the same. Schneier says that the book is basically a first draft at this point, and might still change quite a bit. Some of the comments focus on whether "dishonest" is actually the best term to use for defecting from social norms.