‘The fact that a language originated in 1973 has required as little change as this one has in thirty years of heavy use is truly remarkable, and without parallels anywhere else in computer science or engineering.’1

Xr0 is a tool for proving that C programs are safe at compile time. It relies on semantic abstractions, which are programmer annotations that describe the safety properties of code:

/* the [] part tells Xr0 we're using the heap */
void *
alloc1() [ .alloc result; ]
{
	return malloc(1);
}
$ 0v alloc1.x
$ echo silence is golden
/* error: this allocates but has no [] */
void *
leak1()
{
	return malloc(1);
}
$ 0v leak1.x
qed error: actual and alleged states differ

Xr0 is currently focused on dealing with memory leaks, but in time we intend for it to give C programmers the same safety guarantees that most higher-level languages offer.

Xr0 is

Sounds interesting? Then

Our Sponsors

The Xr0 project is greatful for generous support from

An open-source modern team chat app designed to keep both live and asynchronous conversations organized.


  1. Eric S. Raymond, The Art of Unix Programming, 20 years ago. ↩︎

  2. These figures omit the Lex and Yacc files because they’re hard to assess properly. We’re relying on these tools for now because the Xr0’s syntax is in a state of flux. ↩︎