This paper presents the comprehensive system description of version 2.0 of the Marabou framework, a tool for formal analysis of neural networks. Marabou 2.0 introduces several significant improvements over its predecessor, including a new build/test system, an optimized core architecture, enhanced decision procedures and abstract interpretation techniques, support for a wider range of activation functions, proof production capabilities, additional input formats, and a more powerful Python API. The paper highlights the major features and components of Marabou 2.0, discusses its architecture and core components, and provides a detailed overview of its performance, as demonstrated by the VNN-COMP'23 results and runtime comparisons against an early version of Marabou. Marabou 2.0 is designed to be versatile and user-friendly, suitable for a wide range of formal analysis tasks in the field of neural network verification. The paper also showcases several recent applications of Marabou, such as verifying the Decima job scheduler, formalizing explainability in DNNs, analyzing learning-based robotic systems, producing proof certificates for ACAS-Xu benchmarks, and verifying quantized neural networks. The performance evaluation shows significant improvements in runtime and memory efficiency compared to the early version of Marabou.This paper presents the comprehensive system description of version 2.0 of the Marabou framework, a tool for formal analysis of neural networks. Marabou 2.0 introduces several significant improvements over its predecessor, including a new build/test system, an optimized core architecture, enhanced decision procedures and abstract interpretation techniques, support for a wider range of activation functions, proof production capabilities, additional input formats, and a more powerful Python API. The paper highlights the major features and components of Marabou 2.0, discusses its architecture and core components, and provides a detailed overview of its performance, as demonstrated by the VNN-COMP'23 results and runtime comparisons against an early version of Marabou. Marabou 2.0 is designed to be versatile and user-friendly, suitable for a wide range of formal analysis tasks in the field of neural network verification. The paper also showcases several recent applications of Marabou, such as verifying the Decima job scheduler, formalizing explainability in DNNs, analyzing learning-based robotic systems, producing proof certificates for ACAS-Xu benchmarks, and verifying quantized neural networks. The performance evaluation shows significant improvements in runtime and memory efficiency compared to the early version of Marabou.