  Hybrid systems verification is quite important for developing correct
controllers for physical systems, but is also challenging. Verification
engineers, thus, need to be empowered with ways of guiding hybrid systems
verification while receiving as much help from automation as possible. Due to
undecidability, verification tools need sufficient means for intervening during
the verification and need to allow verification engineers to provide system
design insights.
  This paper presents the design ideas behind the user interface for the hybrid
systems theorem prover KeYmaera X. We discuss how they make it easier to prove
hybrid systems as well as help learn how to conduct proofs in the first place.
Unsurprisingly, the most difficult user interface challenges come from the
desire to integrate automation and human guidance. We also share thoughts how
the success of such a user interface design could be evaluated and anecdotal
observations about it.
