Large neural networks, as solid backbones of many modern ML techniques are appearing inside more and more secure software environments. It is now more than ever important to shine light into their black box behavior and to ensure that their properties stay within certain boundaries. The topic of formal verification of neural networks intends to aim to formally guarantee properties of neural networks such as monotonicity, robustness and correctness. During the session we will briefly cover the primary theoretical background of bound propagation and zonotopes while also giving a short insight to the practical implementations such as alpha-beta-CROWN and nnenum.