# Specification and proof

### From HaskellWiki

(Difference between revisions)

(Added Category:Development tools) |

## Latest revision as of 13:16, 25 May 2013

*This article is a stub. You can help by expanding it.*

## Contents |

## [edit] 1 Introduction

**To do**

## [edit] 2 In the real world

The Australian ICT research center Nicta has developed a verified micro kernel, see the following papers:

## [edit] 3 Papers

## [edit] 4 Software

- Applications and libraries/Theorem provers, tools for formal reasoning, written in Haskell

- The Programatica Project has an expressive logic called P-logic, and tools supporting it

- Sparkle is a theorem prover for the functional programming language Clean

## [edit] 5 E-mail, blog articles

- The thread "Specification and prover for Haskell" on the Haskell mailing list