The memory-processor bottleneck and scaling difficulties of the CMOS transistor have given rise to a plethora of research initiatives to overcome these challenges. Popular among these is in-memory crossbar computing. In this paper, we propose a framework for synthesizing fault-tolerant computation- in-memory circuits based on bounded model checking. The resulting designs can be used to compute Boolean formulas using a constant number of read and write cycles. We demonstrate the effectiveness of the approach by generating addition and comparator circuits in the presence of common crossbar faults.