I would say KLEE is coolest, as it works on LLVM bitcode, so anything you can compile to that, you can verify.
CBMC scales worse (best for smaller modules, not complete systems), but is also very capable.
You can use both as general-purpose solvers for any problem you can formulate in C/LLVM. You assert that there is no solution, run the tool and (unless you run out of time/resources), you get a counter-example refuting the assertion -> which will then be a valid solution.
I’ve used this to find e.g. a sequence of N bytes with a specific (non-cryptographic) checksum etc. They are very powerful tools.
CBMC scales worse (best for smaller modules, not complete systems), but is also very capable.
You can use both as general-purpose solvers for any problem you can formulate in C/LLVM. You assert that there is no solution, run the tool and (unless you run out of time/resources), you get a counter-example refuting the assertion -> which will then be a valid solution.
I’ve used this to find e.g. a sequence of N bytes with a specific (non-cryptographic) checksum etc. They are very powerful tools.