I am curious as to whether Frama-C has been formally verified using Frama-C or another verification framework, since bugs in Frama-C could possibly result in bugs in programs verified by Frama-C going unnoticed.
I understand that the process would be extremely tedious, but given that Frama-C is used in various industries for critical applications like nuclear systems and aviation, I would expect that some organizations would be willing to verify it.
The first part of your question is extremely easy to answer: Frama-C is written in OCaml, and dedicated to verify programs written in C, so that you can't verify Frama-C in Frama-C.
Regarding the verification of Frama-C through other means, there have been various works dedicated to formalize some analyses, but usually only on a subset of C and ACSL. This often includes the Coq proof assistant. A non-exhaustive list of such examples include:
Finally, regarding deployment in industrial domains with stringent constraints (in the form of some certification authority giving some formal -in lawyer's sense rather than mathematical's one- stamp of approval), Airbus and Thales have published papers on how their use of Frama-C helped them in getting their products certified.