I can't give a good, covering answer without writing a wall of text, sorry in advance.
CBMC and KLEE try to statically verify assertions in one of three outcomes:
1. Verified: No counter-example was found, that breaks the assertion(s).
2. Rejected: A counter-example was found, that makes an assertion false.
3. Tool runs forever or exhausts system resources.
That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits.
The modeling language is also just C, which simplifies things HUGELY.
A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.).
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.
ACL2 is also VERY powerful and capable.