While autonomous driving has crossed over a million miles, the liability of accidents involving such self-driving cars is completely on the manufacturer. The central question then is, “Will the vehicle make the best possible decision under all circumstances?” Since the vehicle controller must decide when and how to turn, overtake, merge, stop and accelerate under different driving scenarios, this decision logic is implemented in the decision controller that is above the supervisory controller. The goal of this research is to develop a framework to reason about the safety and performance of the vehicle’s decision controller and to be able to provide quantative bounds on the safety. In other words, we aim to provide a bound on the risk by ensuring that for a given scenario, with the on-board sensor information, the vehicle made the best possible decision in terms of safety and performance. With a combination of modeling vehicle perception and controls, we are developing a tool chain to describe hundreds of driving scenarios and formally verify that in all possible interactions of the vehicles, pedestrians, and other agents - the vehicle decision controller will make a safe decision and not crash.