Using TLA+ for Simulation-proofs

[Mike Clark]

Hi all,

I'm just beginning to learn about TLA+ and trying to understand some of the capabilities it provides and the problems it could be used to solve.

I'm curious if TLA+ could be used for specifying simulation-proofs (e.g., https://eccc.weizmann.ac.il/report/2017/112/). 

I haven't seen much about such a use case discussed online. If it could be used for something like this, any pointers? I'm especially interested in computational indistinguishability in the real/ideal world paradigm.

Mike