Yes, working on distributed database. So far it's quite useful -- it is possible to quickly check correctness of changes that you intend to make in few crucial places in code. It took about a week of learning/experimenting to write a useful spec. Also resulting state machine is not that much different from what you can expect in networking code working with epoll().