The purpose of this page is to collect material related to Perfect Developer, mainly to support the teaching of formal methods at the Technische Universität Wien (see e.g. the course Formale Verifikation von Software/Formal Verification of Software).
Perfect Developer is a tool developed by Escher Technologies. The British company describes its product as follows:
Perfect Developer is an object oriented software development tool for producing software that is mathematically proven to be correct. […] To use Perfect Developer, you construct a model. You use its own language, Perfect, to write your specifications. You specify the model and the requirements, then you either refine the specification to code or let Perfect Developer do it for you. You never write code except as a refinement to the specification! To prove that the software is correct, Perfect Developer attempts to validate the model against the requirements. Any refinement you did is validated against the model.