The figure below presents an architectural overview of our system. Our visualizations are generated by a separate server which communicates with the theorem prover through a simple protocol. The protocol can be implemented in the theorem prover's language providing access to information, as if the visualization server is a regular user.