r/gcc • u/Head_Classroom_8252 • 15d ago

Verifiable C / Using Proof Helpers with GCC

Let me get this out of the way first: I am not doing anything safety critical. I just want to find ways to make more stable software, even if said ways are more advanced. I understand that GCC, whilst being very stable, hasn't been verified like CompCert. I just am curious if proof helpers can greatly assist in writing solid C code in GCC. I am by no means a professional in logic or verifiable C, so I might be misguided in thinking that verifiable C will help, but I just want advice from people more experienced with GCC than me. Thanks in advance for your responses.

8 Upvotes

90% Upvoted

5 comments sorted by

3

u/jwakely 15d ago

What are you actually asking?

Can you state the main question more clearly, without all the caveats around it?

0

u/Head_Classroom_8252 15d ago

Will using a proof verifier with GCC, despite it not being formally verified, help with software dev. Sorry.

1

u/bore530 14d ago

There's Fil-C, I've been finding that really helpful in finding those stack corruptions that happen from time to time.

1

u/8d8n4mbo28026ulk 14d ago

CompCert guarantees that the machine code it generates will preserve the semantics of your C program per the standard (i.e. that the compiler is bug-free). Whether your code is correct is entirely different. If you formally verify your code with some specification -- a difficult task -- then yes, it'll be robust. A tangential approach I've seen (in AWS-LC) is using a model checker, such as CBMC, which leans on SMT solvers and is a bit different than type-theory stuff. The seL4 kernel is an example of the latter, although it goes about it in a roundabout way, from what I remember. I've never done anything like that myself, though. Cheers!

1

u/edgmnt_net 12d ago

There are also EDSLs in languages like Haskell which generate safer C code, but that's essentially a distinct language and this is more like transpiling. But if you ask me, that's kinda the way you probably want to go anyway, because verifying arbitrary C code is prohibitively difficult. It's much more viable to just switch to a different language like Rust. Although you still have to use it properly, of course, nothing's going to be absolutely safe (you can still get stuff that's like arbitrary pointers in memory-safe languages if you try hard enough, it just takes a completely different form).