Using the "C Bounded Model Checker" (CBMC)

[mrash]

Very strong validation of C code can be achieved through the usage of the C Bounded Model Checker (CBMC): https://www.cprover.org/cprover-manual/cbmc/tutorial/

The fwknop project should investigate its use in addition to all of the other security validation techniques it uses.