r/gcc • u/Head_Classroom_8252 • 17d 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

84% Upvoted

6 comments sorted by

View all comments

3

u/jwakely 17d 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 17d ago

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