There's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		LiamPowell on Feb 14, 2025 \| parent \| context \| favorite \| on: Nvidia Security Team: “What if we just stopped usi... 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.

MaxBarraclough on Feb 15, 2025 [–]

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/

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact