Low latency communication is a major challenge when humans have to be integrated into cyber physical systems with mixed realities. Recently, the concept of negative latency has been coined as a technique to use anticipatory computing and performing communication ahead of time. For this, behaviors of communication partners are predicted, e.g., by components trained through supervised machine learning, and used to precompute actions and reactions. In this paper, we approach negative latency as anticipatory networking with formal guarantees. We first establish a formal framework for modeling predictions on goal-directed behaviors in Markov decision processes. Then, we present and characterize methods to synthesize predictions with formal quality criteria that can be turned into negative latency. We provide an outlook on applications of our approach in the settings of formal methods, reinforcement learning, and supervised learning.