The design, implementation, and verification of agent conversations (i.e., multiagent sequences of language primitives which are intended to together achieve some goal) can be difficult and exacting, and often requires skills which agent developers do not possess. In this paper, we describe the architecture of a planned software tool that is designed to help developers with this task. Our proposed Conversation Design Tool (CDT) will be built as a set of extensions to an automatic theorem-proving framework, and so will be able to directly manipulate expressions in a variety of ACL semantics description languages. The CDT will also employ a variety of graphical representations, such as finite state machine diagrams and Petri net diagrams, to facilitate reasoning in certain specialized domains. Finally, the CDT will include a generative capability to automatically create conversation policy configuration files for KAoS-architecture agents.