  There is a great diversity of formal models to understand the dynamics of
transport and vehicular flow on a road. Many of these models are inspired by
the dynamics of flows governed by partial differential equations. However, it
is possible to simplify these models to ordinary equations by considering
constant variations in some of the input variables in this type of models.
However, given that these types of systems present discrete changes when the
vehicle density is altered in some sections of the lane, it seems reasonable to
make use of hybrid systems to better understand the evolution of these
dynamics. In this work we are interested in making use of dynamic differential
logic to formally verify one of these models proposed in ordinary equations.
This verification will be done through a proof assistant specially designed for
hybrid systems called KeYmaera. Once we adapt the model to a hybrid system
representation we proceed to use KeYmaera to verify that the proposed model is
formally correct.
