Analyzing high-dimensional data like camera images is an essential task in modern autonomous systems such as self-driving cars. However, this task, known as perception, is notoriously difficult to perform error-free when it is implemented with neural networks. In fact, there is typically no mathematical definition of what constitutes a correct output or an error. So one cannot precisely check the correctness of such perception or guide its training with precise definitions. This project seeks to overcome the above challenges by rethinking how perception is built, using formal analysis. Specifically, we aim to develop perception in a modeling and training loop, where we (1) create a mathematical model of the perception's inputs and outputs, (2) train a neural network based on this model, and (3) repeat if we cannot automatically prove correctness using a neural network analysis tool.