Proving a program in separation logic consists of tracking how parts of the heap are disjointly accessed by the different parts of the program. Parallelizing a program consists of finding parts of the program which access disjoint parts of the heap. Because proving a program in separation logic and parallelizing this program involve a similar reasoning, it follows that proving a program in separation logic considerably eases the task of automatically parallelizing this program. In this paper we show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. We present an implementation of our algorithms that uses smallfoot as the proof generator and tom as the proof transforming engine. Finally, we show how our technique will benefit of the recent advances in separation logic.