This research aims to show through a detailed case study that scaling up modular verification to component-based software is not only possible, but when combined with appropriate tool support, can be made more comprehensible and practicable to researchers and students in the software engineering (SE) curriculum. The study involves an interplay of multiple components that have novel designs and object-oriented interfaces to encapsulate non-trivial data structures and algorithms. Each component is annotated with formal specifications that are all designed to be modular, reusable, and amenable to automated verification and analysis. The components are constructed using a formalization integrated development environment (F-IDE) that we’ve built for this purpose. Experimental evaluation of the F-IDE itself will be performed in the context of the software engineering curriculum at Clemson University over the course of upcoming semesters, while evaluation of the various components involved in the study will be performed on the basis of the provability of mechanically generated proof obligations.