Programming languages are essential for creating software products such as mobile applications, and computer programs. Although there are many powerful languages available, very few offer the ability to verify the correctness of the program. To ensure programs work correctly, programmers today use testing: they run the program on sample inputs or in sample scenarios, and confirm that the program produces the proper output or expected behavior.  This process generally cannot rule out all possibility of bugs, since the number of possible inputs is usually infinite or too large to test completely. The purpose of this investigation is to show the programming and proving abilities of Trellys. Trellys is a new programming language designed for verification of user-specified properties of programs. For the purpose of this research, we designed, implemented, and verified a simple Lambda Calculus interpreter, a central component of many functional languages such as Haskell and OCaml. A more efficient kind of interpreter, called a CK machine, was also implemented and verified. These results provide further demonstration of the capabilities of Trellys for logically proving properties of software, thus providing programmers with a new and powerful tool for writing reliable programs."