290 Formalization

8 Analysis