formal methods don't magically make a specification bug-free/secure though, nor does it mean you won't making bugs in the formal verification code you're writing.. so what are you actually proving? other than just another layer of testing essentially? can anyone tell a client that a system has been 'proven' correct? I think when we use these words with people who don't completely understand the implications we need to be more precise what that means... that's what leslie lamport is all about ! being precise!