RecordFlux VS acsl-by-example

RecordFlux[0] is a DSL written in Ada for specifying messages in a binary protocol. Code for parsing these messages is then generated automatically with a number of useful properties automatically proven including that no runtime errors will occur.

[0] https://github.com/Componolit/RecordFlux

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,

https://frama-c.com/html/tutorials.html

Has a link to the ACSL-by-example PDF which gives examples of creating in C various C++ STL inspired data structures and routines:

https://github.com/fraunhoferfokus/acsl-by-example/blob/mast...

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.