Motion planning for autonomous vehicles has to be able to cope with various complex requirements from following the rules of the road, avoiding (dynamic) obstacles, dealing with unusual circumstances, as well driving in a socially compliant way. In this talk, we present an approach combining formal methods with traditional motion planning and control algorithms to attack this challenge. We discuss the use of Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) to express traffic rules and driving styles. We present quantitative semantics to recognize the maximally compliant motion plans and algorithms to compute those. In particular, we focus on risk-aware autonomous driving under uncertainty: We suggest a risk measure that captures the probability of violating the specification and determines the average expected severity of violation. Using highway scenarios of the US101 dataset and Responsibility-Sensitive Safety (RSS) model as an example specification, we demonstrate that by incorporating the risk measure into a trajectory planner, we enable autonomous vehicles to plan minimal-risk trajectories and to quantify trade-offs between risk and progress in traffic scenarios.