In this talk I present a stochastic model for human driving behavior and a general (model-based) approach to design a so-called safety supervisor which can override the human driver if otherwise a collision would occur. The main property of our approach is that it provides formal guarantees for the correctness of the safety supervisor. I will illustrate the theory with two application examples.