I've tried SPARK. Compared to Frama-C, SPARK is not as powerful. Frama-C can prove the correctness of arbitrary heap manipulation algorithms. SPARK can handle singly linked lists but not doubly linked lists (last I checked).

Although, usually the people who use SPARK use it because it is certified for their industry (such as aerospace).