In the last few decades, optics and laser technology has been increasingly used in the main stream industrial and research domains such as terrestrial telescopes, biomedical devices and optical communication. The modeling and analysis of such systems is mainly based on the abstraction of light waves, i.e., rays, Gaussian beams or electromagnetic waves. In this project, we propose to use higher-order-logic theorem proving to improve the analysis of Gaussian optical systems which are based on the notion of Gaussuan Beams. In particular, we extend the existing formalization of geometrical optics by the formal specification and verification of the properties of the Gaussian beams in HOL Light theorem prover. In order to demonstrate the effectiveness and use of our work, we present the formal modeling of generalized qausi-optical systems along with the verification of the generic theorems about the Gaussian beam parameters such as beam width radius. Furthermore, we present a case study of the receiver module of the real-world Atacama Pathfinder Experiment APEX telescope.