  Teaching proofs is a crucial component of any undergraduate-level program
that covers formal reasoning. We have developed a calculational reasoning
format and refined it over several years of teaching a freshman-level course,
"Logic and Computation", to thousands of undergraduate students. In our
companion paper, we presented our calculational proof format, gave an overview
of the calculational proof checker (CPC) tool that we developed to help users
write and validate proofs, described some of the technical and implementation
details of CPC and provided several publicly available proofs written using our
format. In this paper, we dive deeper into the implementation details of CPC,
highlighting how proof validation works, which helps us argue that our proof
checking process is sound.
