This is awesome, thanks for sharing.
This sounds very similar to the model-based test case generation approach taken in this MongoDB paper:
https://dl.acm.org/doi/abs/10.14778/3397230.3397233. The main difference here is that Mocket uses annotations in the implementation code to provide a mapping for state variables / actions. I think this is a really good idea, because it removes the need to introduce yet another tool into the workflow. I wonder what limitations exist on the annotations in practice, but it definitely seems like an interesting direction overall.
Re the citations, the paper does cite "How Amazon Web Services Uses Formal Methods," so the authors definitely are aware of Amazon's usage of TLA+. "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" uses property-based testing to generate test cases for the implementation, so it's not exactly an apples-to-apples comparison. I didn't find that this omission took anything away from the paper.