I was working from a design-doc, not code.

"look at @design-document and generate a TLA+ specification for the interactions between local and remote"