I can't remember if it bounds-checks the pointers or just arrays. However, SPARK lets you prove conformance of code to specs and absence of specific error conditions. Here's a linked list example:

http://www.spark-2014.org/entries/detail/spark-2014-rational...

There's also formal verification work on linked lists. If any have simple VC's, they could be encoded in containers like above as well. Tools exist to do similar stuff for C, too.