In previous years I have discussed my attempts to apply model-checking formal-verification techniques to multi-agent systems. These attempts have been a useful exercise, but have always suffered from the state space explosion problem or a lack of expressiveness. I have recently revisited this problem by applying model checking to the dialogue protocols which we have been developing. This allows us to address the problems of asynchrony, and to prove the correctness of the protocols. In my talk I will discuss my initial attempts at model checking these protocols and demonstrate that this approach appears to yield useful results.