I'm a poor person looking for an advice.
I know this is the right place since all of you have huge expertise in formal verification.
I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. 

Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?