Following the release of Frama-C 26.0 (Iron), [MetAcsl](/fc-plugins/metacsl.html)[v0.4](https://git.frama-c.com/pub/meta/-/releases/0.4) is out. The corresponding `opam` package should be available soon.
MetAcsl intends to provide simple and compact ways to express properties that
would demand peppering the code with thousands of annotations in plain ACSL.
Its main use cases focus on security properties (notably ensuring that
write and read accesses to sensitive memory locations are guarded appropriately).
Feel free to consult its [homepage](/fc-plugins/metacsl.html) for more information.
