  Technology advances give us the hope of driving without human error, reducing
vehicle emissions and simplifying an everyday task with the future of
self-driving cars. Making sure these vehicles are safe is very important to the
continuation of this field. In this paper, we formalize the
Responsibility-Sensitive Safety model (RSS) for self-driving cars and prove the
safety and optimality of this model in the longitudinal direction. We utilize
the hybrid systems theorem prover KeYmaera X to formalize RSS as a hybrid
system with its nondeterministic control choices and continuous motion model,
and prove absence of collisions. We then illustrate the practicality of RSS
through refinement proofs that turn the verified nondeterministic control
envelopes into deterministic ones and further verified compilation to Python.
The refinement and compilation are safety-preserving; as a result, safety
proofs of the formal model transfer to the compiled code, while counterexamples
discovered in testing the code of an unverified model transfer back. The
resulting Python code allows to test the behavior of cars following the motion
model of RSS in simulation, to measure agreement between the model and
simulation with monitors that are derived from the formal model, and to report
counterexamples from simulation back to the formal model.
