Hacker News Reader

Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.

View on HN

There's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick SPARK any day. Having a rich type system and not having to work with pointers makes proving a program so much easier.

Right, Frama-C can formally prove properties of C code.

There are also proprietary solutions that do something similar:

• https://www.eschertech.com/products/ecv.php

• https://www.trust-in-soft.com/

Reply on news.ycombinator.com