Welcome to CN¶
These tutorials and docs were developed by Christopher Pulte, Benjamin C. Pierce, and Cole Schlesinger, with contributions from Elizbeth Austell.
BibTeX
CN is an extension of the C programming language for testing and verifying the correctness of C code, especially on low-level systems code. Compared to standard C, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes safely — does not raise C undefined behaviour — and correctly — satisfying to strong, user-defined specifications.
CN provides utilities for verifying specifications at compile time as well as automatically generating unit and integration tests to test specifications at runtime.
This documentation is a work in progress -- your suggestions are greatly appreciated!
-
Set up in 5 minutes
Build and install CN and get up and running in minutes
-
Your first spec
Check out the Basic Usage tutorial to write, test, and verify your first spec
-
Tutorials
Find tutorials covering common tasks and introducing CN features
-
Language reference
Quick reference for CN specification syntax
Origins and papers¶
CN was first described in CN: Verifying Systems C Code with Separation-Logic Refinement Types by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami, in POPL 2023. The Fulminate system for runtime testing of CN specifications was first described in Fulminate: Testing CN Separation-Logic Specifications in C, by Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell, in POPL 2025. To accurately handle the complex semantics of C, CN builds on the Cerberus semantics for C. Some of the examples in this tutorial are adapted from Arthur Charguéraud’s excellent Separation Logic Foundations textbook, and one of the case studies is based on an extended exercise due to Bryan Parno.
Acknowledgment of Support and Disclaimer¶
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, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
Building these docs¶
These docs are built with Material for MkDocs. To build and serve them locally on http://localhost:8000:
# Install Material for MkDocs
pip install mkdocs-material
# In the cn-tutorial root directory, run
mkdocs serve
Docs layout¶
mkdocs.yml # The configuration file.
docs/
README.md # The documentation homepage.
... # Other markdown pages, images and other files.