This is the aim of computer aided formal reasoning. To provide the user with tools for representing arbitrary systems and specifications, in which representing properties of various kinds of systems. The tool will allow the user to develop proofs in an interactive way and to build in this way proof objects. And those proof objects will be in the end automatically checked.

---