We have written a few tutorials to show how codex can be used and extended.
There is a short quick start tutorial that shows the steps needed to run Frama-C/codex on a simple C file. For a more in depth look at the interface, check out the types tutorial.
The while tutorial describes how Codex's components can be used to build an analyzer for a simple imperative while language. Along the way, it introduces many of the core components of codex. It is mostly intended for developers who want to use or extend the codex library.
The types tutorial presents Codex's refinement type system and how it can be used to precisely specify memory layouts. It was written to accompany the OOPLSA 2024 paper. It also describes the Frama-C/Codex and Binsec/Codex interfaces (command line arguments, terminal and HTML outputs...).
It covers in particular:
This one is more targeted to users wishing to use Codex to verify C or binary code.