Symbolic datatypes are central to abstract reasoning about dynamical systems. Successful examples include BDDs and SAT for finite-state systems, and polyhedra and SMT for discrete dynamical systems over certain infinite state spaces. Neural networks provide a natural symbolic datatype over continuous state spaces, with the added benefit of supporting key operations while being trainable. We advocate using neural networks for multiple purposes in reasoning about continuous state spaces, particularly for representing both deterministic dynamics—such as controllers—and correctness certificates. A correctness certificate is a succinct witness for a desired property of a dynamical system. For example, invariants and barrier functions certify safety, while Lyapunov functions and supermartingales certify progress. Stochastic barrier functions and supermartingales can further account for uncertainty (noise) in system dynamics. Established techniques from machine learning and formal reasoning about neural networks—such as SMT, abstract interpretation, and counterexample-guided refinement—enable the joint synthesis of controllers and correctness certificates. This allows for the synthesis of guaranteed-to-be-correct controllers, where both the controllers and their certificates are represented, learned, and verified as neural networks. This talk includes joint work with Krishnendu Chatterjee, Mathias Lechner, and Djordje Zikelic.