I used TLA+ in a (hobby) web app by asking it to model the endpoints and the data user can get from them, and then what kind of access that data can grant in the system, and then implement some properties over that kind of data. I suppose basically like "you can't get access to another user's shopping basket", although mine was maybe a bit more convoluted.