"Verifying lambda-calculus abstract machines in Trellys" sounded like Greek to undergraduate researcher Angello Astorga at the start of his summer undergraduate research work with Prof. Aaron Stump.