TITLE: Degrees of trustworthiness: observations arising from the SPARK proof tools and their use Ian O'Neill Altran Praxis Ltd ABSTRACT: SPARK is an annotated subset of Ada, which is in use in a range of high-integrity software development. SPARK's annotations form a 'contract' for the software, supporting both proof of partial correctness and the more tractable goal of proof of freedom from a class of run-time errors. The SPARK proof tools -- a short-rein interactive theorem prover (the SPADE Proof Checker) and a non-interactive prover (the Simplifier) have been in existence and in use on real software development projects for more than two decades. The main aim of this talk will be to consider issues of trustworthiness in proof with the SPARK proof tools, illustrated with real examples from practical experience. The talk will commence with a brief summary of the nature of SPARK's support for programming by contract, and the origins of the proof tools and work done initially to establish their soundness. We will consider examples of the verification conditions that arise in practice in proofs of exception-freedom in particular, the success rate of the Simplifier in discharging these and some examples which do not get discharged automatically for various reasons. We will then consider how a class of extensions to the power of the Simplifier have been made, what drove these extensions and how the soundness of these have been established. A further extension, allowing users to write their own extensions (proof rules) will also be considered, with examples from practical project experience and the issues that arise. We conclude with a look at current limitations in the field of proof of exception-freedom for code using SPARK floating point types and subtypes, including what can be done in practice to work around these limitations and support proof of exception-freedom in particular.