[debugnik]

Not a library, but it kinda does: Frama-C will formally verify C code using special comments to write the contracts in, and I hear it can prove more pointer properties than SPARK, although it takes more more effort to maintain a Frama-C codebase due to all the other missing language features.

[johnisgood]

Does that mean I can use C + Frama-C so I won't have to use Rust (or Ada / SPARK)? :P