Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods. Epigram is freely available this page provides access to downloads of version 1 as source or binaries for the major platforms along with relevant documentation. Development on version 2 is under way we hope this will considerably improve on the first, and details of its current state are available, in the form of a developers' 'blog.