Hacker News Reader

Yes, there are hand-written (i.e. not mechanised) proofs that the transformations are sound. But there are no proofs about CryptoVerif's actual code.

Have those handwritten proofs been published?

Yes, the proofs have been published at peer-reviewed conferences. Let me look for the exact references tomorrow.

The proofs are in this paper [1], see Section 3 “Game Transformations” and Appendix E.

Thanks.

Interestingly, that paper uses a variant of pi-calculus, i.e. an idealised programming language for message passing, as 'games'.