Separation logic is used to prove heap safety in low-level code, esp with pointer manipulation. This tool claims fast, sound, thorough analysis. It’s also formally verified. They claim it’s retargetable for other static analyses.

Note: Title changed to be more clear what this does.