Autonomous vehicles need to be designed to abide by the same rules that humans follow. This is challenging, as traffic rules are fuzzy and not specified at a level of detail to be comprehensible for machines. Without proper formalization, satisfaction cannot be implemented in a planning component, nor can it be monitored and verified during simulation or testing. However, no work has provided a complete set of machine-interpretable traffic rules for a given operational driving domain. We propose a methodology on how to legally analyze and formalize traffic rules in a formal language. We use Linear Temporal Logic as a formal specification language to describe temporal behavior, thus capable of capturing a wide range of traffic rules. We contribute a formalized set of traffic rules for single-direction carriageways, such as on highways. We then test the effectiveness of our formalized rules on a public dataset.