Prophecy variables were introduced in the article “The Existence of Refinement Mappings” by Abadi and Lamport. They were difficult to use in practice. We describe a new kind of prophecy variable that we find much easier to use. We also reformulate ideas from that article in a more mathematical way.

@article{paperbot1618,
  title = {Prophecy Made Simple},
  author = {Leslie Lamport and Stephan Merz},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {44},
  number = {2},
  year = {2022},
  doi = {10.1145/3492545}
}