I was reading about proof assistants, formal verification etc, also I have a lambda calculus implementation. My question is: Is it possible to *prove* that my implementation is correct?

In fact I have two implementations, having a single proof for both would be nice but I have no idea how to attack the problem. What I know is that all possible inputs are infinite, but, the rules of lambda calculus are finite. Can I implement only the sets that verify that these rule are holding and this way prove that the whole implementation is correct?