Welcome to the Wiki for Checked C! This Wiki is current and actively maintained as of August 2024.

Checked C is an opt-in extension to C that adds bound checking and type safety. This helps programmers write more secure and reliable code. This Wiki contains:

• An overview of the Checked C extension and how to use it.
• Suggestions for converting existing C code to Checked C.

For developers with existing C codebases, 3C (Checked-C-Convert) software facilitates the transition to Checked C by inferring as many Checked C annotations as possible and guiding you through the assignment of the remaining ones. A detailed specification is here.

For a deeper understanding of 3C, refer to the 3C documentation. Note that 3C is in its pre-alpha stage as of March 2021, but is under active development.

A detailed specification is available here.

• For some simple code, see the samples directory.

• For some more complicated examples, see our Checked C translations of the Olden and PtrDist benchmarks.

• To see some real-world C code that has been converted to Checked C, see

  • The Checked C fork of the parson JSon parser.
  • The Checked C branch of the Microsoft Research Robust Internet of Things (RIoT) project. In this branch, the cryptography code has been converted to use Checked C.

  -For some in-progress conversions to Checked C, see the conversions of one of the following code bases to Checked C:

  1. Vsftpd (re-port branch)
  2. Lua (checkedc-port branch)
  3. The Checked C fork of the musl C library.
  4. The Checked C fork of libc-test. Used to test the conversion of musl to Checked C.

To use Checked C, currently you need to build your own copy of the compiler. Directions are here.

Checked C is an open-source research project. Anyone with time or interest can participate. Trying out Checked C, reporting bugs, and giving us feedback is helpful. There are other ways to contribute too.