  Many verification tools come out of academic projects, whose natural
constraints do not typically lead to a strong focus on usability. For
widespread use, however, usability is essential. Using a well-known benchmark,
the Tokeneer problem, we evaluate the usability of a recent and promising
verification tool: AutoProof. The results show the efficacy of the tool in
verifying a real piece of software and automatically discharging nearly two
thirds of verification conditions. At the same time, the case study shows the
demand for improved documentation and emphasizes the need for improvement in
the tool itself and in the Eiffel IDE.
