Using TLA+ for Simulation-proofs

27 views

Skip to first unread message

Mike Clark

unread,

Mar 11, 2021, 12:09:47 PM3/11/21

to tlaplus

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.