CN

CN is a tool for verifying that C code is free of undefined behaviour and meets user-written specifications of its ownership and functional correctness, and for translating those specifications into C assertions that can be checked at runtime on concrete test cases. It builds on the Cerberus C semantics.

Papers

• Evaluating a Lua runtime for CN separation-logic testing in Fulminate. Muhammad Saljuk Gondal. Thesis for MPhil at the University of Cambridge, 2026. [ pdf ]
• Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows. Zain K Aamer*, Rini Banerjee*, Hiroyuki Katsura*, David Kaloper-Meršinjak*, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C Pierce, Christopher Pulte, Peter Sewell. In PLDI 2026. *these authors contributed equally [ doi | pdf ]
• Translating CN Separation Logic Lemmas to the Rocq Proof Assistant. Amy Yin. Thesis for MPhil at the University of Cambridge, 2025. [ pdf ]
• Model-free Stateful Random Testing. Ethan Chou. Thesis for MSc at the University of Maryland, 2025. [ doi | pdf ]
• Bennet: Randomized Specification Testing for Heap-Manipulating Programs. Zain K Aamer and Benjamin C. Pierce. In OOPSLA 2025. [ doi | pdf ]
• Fulminate: Testing CN Separation-Logic Specifications in C. Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell. In POPL 2025. [ doi | pdf ]
• CN: Verifying systems C code with separation-logic refinement types. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. In POPL 2023. [ doi | project page | pdf ]

Tutorial

See the tutorial documentation.

Installation

Below are the installation instructions for installing CN, and its dependencies.

Docker images

Pre-built Docker images of CN are published to GitHub Container Registry under ghcr.io/rems-project/cn. The CI publishes release-ubuntu, release-redhat, and release-devcontainer tags for both linux/amd64 and linux/arm64. For example, to pull and start an interactive shell with the Ubuntu image:

docker pull ghcr.io/rems-project/cn:release-ubuntu
docker run --rm -it ghcr.io/rems-project/cn:release-ubuntu

The release-devcontainer tag is the image used by the VS Code Dev Container configuration in .devcontainer/.

Installing from source

1. Install make, git, GMP library, pkg-config and either/both Z3 or CVC5. On an Ubuntu system this is done via

   sudo apt install build-essential libgmp-dev pkg-config z3
   

   Note: there is a known bug with Z3 version 4.8.13 (the default on Ubuntu 22.04) so you may wish to install Z3 via opam later for a more up-to-date version. Z3 that is provided in the docker images is sufficiently up-to-date.

2. Install the opam package manager for OCaml: https://ocaml.org/docs/installing-ocaml#install-opam. On Ubuntu 25.04 or later, sudo apt install opam. Older Ubuntu versions have outdated versions of opam, so for those, follow the opam instructions.

3. Initialise opam with a recent version of OCaml (the CI builds with 4.14.1, CN developers use 5.2.0).

   opam init --yes --compiler=5.2.0
   

   Make sure you follow the instructions provided at the end of the output of opam init to complete the initialisation. Typically, on Unix, this is:

   eval $(opam env)
   

4. Clone the CN repo:

   git clone https://github.com/rems-project/cn.git
   

5. For CN end users, who don't want to tinker with CN locally:

   opam install --yes ./cn.opam # z3 for a more recent version
   

6. For CN developers:

   opam install --deps-only ./cn.opam ocamlformat.0.27.0 # one time
   make install # after any edits
   

   which installs CN (as both a library and an executable), and dependencies.

   (If you update CN, you may also need to update its local version of cerberus-lib to stay in sync, by re-running the opam install step above.)

   CN needs clang >= 13.0.0 or gcc >= 8.1 for development.

Contributing

Please see our contributing guide for logistics and our onboarding guide for learning the code base.

Funding

This software has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme from grant agreement no. 101002277 "TypeFoundry", and no. 789108, ERC-AdG-2017 "ELVER"; from the UK Research and Innovation (UKRI) under the UK government’s Horizon Europe funding guarantee for ERC-AdG-2022, EP/Y035976/1 "SAFER"; from an EPSRC Doctoral Training studentship; from Google; and from a Royal Society University Research Fellowship URF\R1\241195 (Pulte).

This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the AFRL and DARPA.

This work was supported by the NSF under grant SHF: Medium: Usable Property-Based Testing, NSF #2402449.