Here is a project that uses F* (another language with dependent types) for proving cryptographic algorithms. https://project-everest.github.io/

As cool as Idris is, in my experience it has been quite buggy. I would suggest Agda or Coq instead which are more mature.