Computer-based counseling systems in health care play an important role in the toolset available for doctors to inform, motivate and challenge their patients according to a well-defined therapeutic goal. In order to study value, use, usability and effectiveness of counseling systems for specific use cases and purposes, highly adaptable and extensible systems are required, which are – despite their flexibility and complexity – reliable, robust and provide exhaustive logging capabilities. We developed a computer-based counseling system, which has some unique features in that respect: The actual counseling system is generated out of a formal specification. Interaction behavior, logical conception of interaction dialogs and the concrete look & feel of the application are separately specified. In addition, we have begun to base the formalism on a mathematical process calculus enabling formal reasoning. As a consequence e.g. consistency and termination of a counseling session with a patient can be verified. We can precisely record and log all system and patient generated events; they are available for advanced analysis and evaluation.