When I write an algorithm I usually write down invariants in comments.
For example, one function might return an ordered list, and the other one expect that a list would be ordered.
I'm aware that theorem provers exists, but I have no experience using them.
I also believe that smart compiler [sic!] can make use of them to optimize the program.
So, is it possible to write down invariants and make compiler check them?
Well, the answer is yes and no. There's no way to just write an invariant separate from a type and check it. There was an implementation of this in a research fork of Haskell called ESC/Haskell, however: http://lambda-the-ultimate.org/node/1689
You do have various other options. For one, you can use asserts: http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html
Then with the appropriate flag, you can turn off these asserts for production.
More generally, you can encode the invariants in your types. I was going to add more here, but dons beat me to the punchlines.
One more example is this very nice encoding of red-black trees: http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/