Games is the terminology of cryptographers, that's why we use it in our work; we need it to interface with this community. The reason this term is used in cryptography might be historical, but also, speaking of an adversary that should not be able to win a security game stays intuitive and thus useful for the definition of security properties.

The language of CryptoVerif is a probabilistic process calculus with interaction by message passing.

Your description of CryptoVerif's output and the proof technique is accurate, thanks that you detailed it for fellow readers. I like the comparison to optimising compilers. In our case, we look at the distribution of messages that are observable by the adversary, and prove that these distributions are only distinguishable with negligible probability. The computations done are actually changed such that they would no longer be useful in a real-world protocol. Like, in one proof step we replace the result of an encryption by a randomly generated bitstring. And if the encryption scheme is secure, the adversary is not able to distinguish these two cases.