I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve.

SPARK does not allow doubly linked lists:

https://blog.adacore.com/pointer-based-data-structures-in-sp...

  For example, singly-linked lists and trees are supported whereas
  doubly-linked lists are not.

With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.

However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.

AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:

https://github.com/AdaCore/why3

And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:

https://github.com/gcc-mirror/gcc/tree/master/gcc/config

Compare with CompCert, the formally verified C compiler:

https://github.com/AbsInt/CompCert

Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:

https://softwarefoundations.cis.upenn.edu/