Yes, a compiler written in C could be verified with Frama-C, but "verifying in Frama-C" for something that hard (i.e. has many proof steps that cannot be automated) really means verifying in a proof assistant that can interact with Frama-C that understands ACSL, and Coq is usually used. And indeed, the loop invariants you mention usually cannot be automatically proved and must be proved manually, which is why there is such a learning curve to Frama-C. I first started using Frama-C without having used Coq/Gallina/OCaml, and I began to learn them simply because I hit a roadblock with Frama-C where I couldn't really progress without a deeper understanding for why automatic proving fails when it fails, why the error messages when automatic proving fails often aren't terribly helpful, what the current limits of automatic proving are, how the automatic proving actually works under the hood, etc.
Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.
I've been slowly working through the Software Foundations series on using Coq/Gallina:
Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction:
also, what happens when the loop invariants can't be automatically proved? is there some way to manually prove invariants hold?