We present a framework for online coordinated obstacle avoidance with formal safety guarantees. Such a formally verified trajectory planner can be used in shared human-robot workspaces to guarantee safety. The obstacle avoidance is based on estimation of the human occupancy on two different time scales. A long-term plan is created based on a probabilistic task representation, learned by demonstration, and a liberate estimate of the human occupancy to be avoided. Using an additional overapproximative, short-term prediction of human motion we guarantee that the robot can always account for sudden or reflex movements. We demonstrate our two-level obstacle avoidance in simulation. The results show that our method reduces the number of safety stops one would encounter when using only the formal safety verification, and generates coordinated alternative movement plans.