This project is a collaborative effort that brings together expertise in formal methods, machine learning, computer-aided design, and fabrication of in-memory computing systems. The main goal of the project is to create formal methods that can synthesize neural networks in the memory of the computer and also prove their correctness. The project pursues tasks that include the verification of neural networks accelerated using analog in-memory computing (IMC) and the synthesis of hybrid analog-digital IMC for neural networks using formal methods and machine learning. The project demonstrates these innovations using in-field fabrication of IMC systems. The effort creates new algorithms for enabling the deployment of robust AI models on emerging in-memory hardware technologies that may be more prone to errors than traditional CMOS technologies. The project would also allow the training of neural networks with reduced power consumption. This is particularly important given the larger adoption of AI and the need to train more and more powerful neural networks. The endeavor enables several other contributions to the research community, including enhancing the reliability of neural networks on in-memory circuits, increasing diversity in computer engineering and computer science, and fostering interdisciplinary collaboration across formal methods, machine learning, and hardware design. The project focuses on advancing formal methods to tackle real-world challenges encountered in em