This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. It categorizes formal control synthesis problems based on system models (deterministic, non-deterministic, stochastic) and formal safety-critical specifications (logic, real-time, real-valued). The review covers fundamental techniques such as abstraction-based and abstraction-free methods, explores data-driven synthesis, and discusses multi-agent systems (MAS) with scalability challenges. Recent trends and research challenges are highlighted, emphasizing the need for fully automated and correctness-guaranteed control synthesis. Formal methods, which use mathematically rigorous techniques, are essential for ensuring safety in autonomous systems, particularly in cyber-physical systems with hybrid dynamics. The paper discusses linear-time and branching-time specifications, such as Linear Temporal Logic (LTL), Metric Temporal Logic (MTL), and Signal Temporal Logic (STL), and their applications in control synthesis. It also covers abstraction-based synthesis, reactive control synthesis, probabilistic synthesis, and data-driven approaches, including reinforcement learning and neural networks. The paper concludes with a discussion of challenges in formal synthesis for autonomous systems, including scalability, safety guarantees, and the integration of formal methods with data-driven techniques.This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. It categorizes formal control synthesis problems based on system models (deterministic, non-deterministic, stochastic) and formal safety-critical specifications (logic, real-time, real-valued). The review covers fundamental techniques such as abstraction-based and abstraction-free methods, explores data-driven synthesis, and discusses multi-agent systems (MAS) with scalability challenges. Recent trends and research challenges are highlighted, emphasizing the need for fully automated and correctness-guaranteed control synthesis. Formal methods, which use mathematically rigorous techniques, are essential for ensuring safety in autonomous systems, particularly in cyber-physical systems with hybrid dynamics. The paper discusses linear-time and branching-time specifications, such as Linear Temporal Logic (LTL), Metric Temporal Logic (MTL), and Signal Temporal Logic (STL), and their applications in control synthesis. It also covers abstraction-based synthesis, reactive control synthesis, probabilistic synthesis, and data-driven approaches, including reinforcement learning and neural networks. The paper concludes with a discussion of challenges in formal synthesis for autonomous systems, including scalability, safety guarantees, and the integration of formal methods with data-driven techniques.