Abstract

Optical resonators are fundamental components used in many safety-critical optical and laser applications such as laser surgery, process industry and nuclear reactors. Due to the complexity and sensitivity of optical resonators, their verification poses many challenges to optical engineers. Traditionally, the stability analysis of such resonators, which is the most critical design requirement, has been carried out by paper-and- pencil based proof methods and numerical computations. However, these techniques cannot provide accurate results due to the risk of human error and inherent incompleteness of numerical algorithms. In this paper, we propose to use higher-order logic theorem proving for the stability analysis of optical resonators. Based on the multivariate analysis library of HOL Light, we formalize the notion of light ray and optical system (by defining medium interfaces, mirrors, lenses, etc.). This allows us to derive general theorems about the behaviour of light in such optical systems. In order to illustrate the practical effectiveness of our work, we present the formal analysis of Fabry-Pérot resonator with fiber rod lens.

HOL Light Script

Core Formalization

• utilities.ml (This file contains some useful tactics which are used in our formalization)
• geom_optics.ml (This file contents the formalization of underlying theory of geometrical optics)

Applications

1. Fabry Perot Resonator with Fiber Rod Lens

Description is given in the papers
• fp_fiber_rod.ml

2. Fabry Perot Resonator with Curved Mirrors



Fabry Perot resonators usually consist of two plane mirrors separated by a certain distance. But this architecture is divergent due to plane mirrors. In our application, we consider the most recent architecture which consists of two curved mirrors
• fp_curved.ml

3. Z-Shaped Resonator



Z-Shaped optical resonators are mostly used in self model locking in lasers. Here, we analyze the most general architecture which consists of two plane mirror and two curved mirrors
• z_resonator.ml