do you know if anyone has used frama-c to verify properties as "deep" as those done by seL4, like functional correctness and integrity, rather than a "shallower" property like memory safety or absence of crashes?
Yes, Frama-C uses a plugin architecture, and there are plugins to verify all kinds of things, including functional correctness. The Frama-C tutorials page,
Also, it is less effort to write bug-free code in OCaml than C. The Coq/Gallina proof assistant even has an OCaml-extraction (and also Haskell-extraction) feature where you extract runnable code from a formally verified algorithm in the Gallina specification language. (It's generally easier to proof theorems about code in the theorem prover itself, go figure.) Most of these C verification tools are written in OCaml, not C, with varying levels of assistance from Coq/Gallina.
The main reason the functional languages make it easier is because you generally execute side-effect free functions on data structures to give them the mathematical property you want. For example, you execute a lexicographical sort function on a list of strings and then the strings in the list all satisfy the mathematical property of a total ordering. You don't have to do any reasoning about the "in-between state" where pointers under the hood are being manipulated, and you don't have to add pre-conditions and post-conditions about the global environment if the code is side effect free and does not access non-local memory.
"Big" software is mostly not difficult algorithms, but writing boilerplate glue code that connects the inputs and outputs of algorithms/functions that are usually written by someone else. Frama-C can definitely verify the boilerplate for "big" software, this is actually easier than verifying data structures and algorithms, which requires knowing the key property to get the prover to see that the algorithm always makes progress toward a solution. Once you have the contracts set up for calling a function, Frama-C will enforce that the contract is always met.
The CompCert verified C compiler is "big" software, but not actually written in C, rather OCaml and Coq/Gallina.
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:
