We apply formal specification and verification techniques for checking correctness properties of artificial pancreas control algorithms. Formal specification and verification techniques attempt to systematically and exhaustively explore the behaviors of closed loop in silico models to understand the worst case effects of disturbances such as meals, external boluses, sensor noise, pressure induced sensor attenuation and set failures on the predicted blood glucose levels of a “virtual” patient.