C verification

Aristotle can formally verify properties of programs written in C. The default deliverable is memory safety: a machine-checked proof that a function executes without undefined behavior (out-of-bounds reads and writes, null or dangling pointer dereferences, uninitialized reads, signed integer overflow, and so on) whenever its callers meet a stated set of preconditions. On request, Aristotle also proves functional correctness: that a function computes what you say it should. Properties are written informally in English, either in the prompt or in a specification file uploaded with your sources.

After analysis Aristotle returns a summary listing, for every function it proved, what was proved and the obligations the caller must meet, along with any behavior of external libraries that was assumed rather than verified. If a memory-safety property is found to be false, you are returned a small standalone C program that fixes the failing inputs and calls your original implementation, so you can reproduce the violation locally with a sanitizer.

Installation

Install the aristotlelib package and set up your API key as described in the installation guide; C verification needs no extra setup.

Example workflow

This example uses a fixed-capacity ring buffer, split across a header ring_buffer.h:

#ifndef RING_BUFFER_H
#define RING_BUFFER_H

#include <stddef.h>
#include <stdint.h>

#define RB_CAPACITY 8

typedef struct {
    uint32_t data[RB_CAPACITY];
    size_t   head;   /* index of the oldest element   */
    size_t   count;  /* number of elements stored      */
} ring_buffer;

void rb_init(ring_buffer *rb);
int  rb_push(ring_buffer *rb, uint32_t value);
int  rb_pop(ring_buffer *rb, uint32_t *out);
size_t rb_size(const ring_buffer *rb);

#endif

and an implementation ring_buffer.c:

#include "ring_buffer.h"

void rb_init(ring_buffer *rb) {
    rb->head = 0;
    rb->count = 0;
    for (size_t i = 0; i < RB_CAPACITY; i++) {
        rb->data[i] = 0;
    }
}

/* Returns 1 on success, 0 if the buffer is full. */
int rb_push(ring_buffer *rb, uint32_t value) {
    if (rb->count == RB_CAPACITY) {
        return 0;
    }
    size_t tail = (rb->head + rb->count) % RB_CAPACITY;
    rb->data[tail] = value;
    rb->count++;
    return 1;
}

/* Returns 1 on success, 0 if the buffer is empty. */
int rb_pop(ring_buffer *rb, uint32_t *out) {
    if (rb->count == 0) {
        return 0;
    }
    *out = rb->data[rb->head];
    rb->head = (rb->head + 1) % RB_CAPACITY;
    rb->count--;
    return 1;
}

size_t rb_size(const ring_buffer *rb) {
    return rb->count;
}

To specify the intended behavior, create a file ringbuf_spec.md alongside the sources:

# Formally Verify the Ring Buffer

Verify that every function in `ring_buffer.c` is memory safe. Callers guarantee that
`rb` points to a valid, writable `ring_buffer` that was initialized with `rb_init`,
and that `out` in `rb_pop` points to writable storage for one `uint32_t`.

Additionally verify the following functional properties:

- After `rb_init(rb)`, `rb_size(rb)` returns 0.
- `rb_push` returns 0 and leaves the buffer unchanged when `rb_size(rb) ==
  RB_CAPACITY`; otherwise it stores `value`, returns 1, and `rb_size` increases by
  exactly one.
- `rb_pop` returns 0 and leaves the buffer unchanged when `rb_size(rb) == 0`;
  otherwise it writes the oldest stored value to `*out`, returns 1, and `rb_size`
  decreases by exactly one.
- Values are returned by `rb_pop` in the same order they were stored by `rb_push`
  (FIFO).
- `rb_size(rb)` never exceeds `RB_CAPACITY`.

Place the three files in a directory on their own and submit that directory. The CLI uploads the directory, except what an ignore rule matches and a few kinds of file it never sends, such as files named like credentials. In a git repository, git's ignore rules apply; elsewhere, or in a folder git ignores, only the directory's top-level .gitignore does. Add --include-ignored to upload what the ignore rules match too, such as headers a build generates. A link to a file goes up only when the file it points to does too, and a link to a folder never does. Include every header the sources need and nothing unrelated:

$ aristotle submit "Perform the formal verification of ring_buffer.c as specified in ringbuf_spec.md" --project-dir ./ringbuf --wait --destination ringbuf_result.tar.gz

Note: mention any relevant compiler flags (-D, -I, -fno-strict-aliasing, -ffp-contract=off, -fwrapv, etc.) or include your build script. Also include header files, API docs, and relevant conceptual docs for your code's non-open-source dependencies. Also include source code and/or Linux/x86-64 binaries for all transitive non-open-source dependencies, if you want Aristotle to check whether a bug in your code can be triggered in your setup.

aristotle submit leaves out files whose names end in .o or .so, even with --include-ignored. Other binaries, such as static libraries (.a), executables, and versioned shared libraries like libz.so.1, follow the ignore rules like any other file, so pass --include-ignored if an ignore rule matches them. To list what would go up without sending anything, run the command with --dry-run in place of --wait and --destination.

Aristotle detects C verification from the .c files in the upload. The command creates a project which you can monitor at https://aristotle.harmonic.fun/projects. Without --wait the command returns immediately after creating the project; use aristotle list, aristotle show <project-id> and aristotle download <project-id> to follow up later.

Before it begins proving, Aristotle reads your sources, builds the call graph from the functions you named, and may ask a small batch of clarifying questions on the project page: which functions are the verification targets, what each entry point may assume about its arguments where the code does not check (non-null, buffer sizes, NUL termination, value ranges), and whether any third-party library your code calls should be verified from its source or relied upon through an agreed contract. Questions are phrased entirely in terms of your own function and variable names. Aristotle may ask them while it works, whether or not you pass --wait, and waits up to 15 minutes for each answer. With --wait at a terminal, the CLI also shows each question as it arrives and sends your answers. Without it, the command prints aristotle questions <project-id>, which lists the questions and lets you answer them. If a question gets no answer in time, Aristotle carries on without it: it verifies what doesn't need a decision only you can make, leaves the rest unverified, and names the open question in its summary. Standard C library calls covered by a built-in contract need no such decision; a missing or inadequate one does. For a batch run nobody will answer, pass --no-questions: Aristotle then asks nothing, and treats each open decision the same way.

For a run where all the properties are proved you will see a summary like this:

## Formal Verification Complete

All 4 functions in `ring_buffer.c` are proved memory safe, and every requested
functional property is proved, under the caller obligations listed below. Each
result has a complete machine-checked proof. The results concern the sources as
submitted.

### Memory safety (4 functions)
- **`rb_init`** — memory safe provided `rb` points to a writable `ring_buffer`.
- **`rb_push`** — memory safe provided `rb` points to a writable `ring_buffer` with
  `count <= RB_CAPACITY` and `head < RB_CAPACITY`.
- **`rb_pop`** — memory safe provided `rb` satisfies the same invariant and `out`
  points to writable storage for one `uint32_t` that does not overlap `*rb`.
- **`rb_size`** — memory safe provided `rb` points to a readable `ring_buffer`.

### Functional correctness
- `rb_init` establishes `count == 0` and `head == 0`; `rb_size` then returns 0.
- `rb_push` returns 0 and modifies nothing when `count == RB_CAPACITY`; otherwise
  it writes `value` at index `(head + count) % RB_CAPACITY`, increments `count`,
  and returns 1.
- `rb_pop` returns 0 and modifies nothing when `count == 0`; otherwise it writes
  `data[head]` to `*out`, advances `head` modulo `RB_CAPACITY`, decrements `count`,
  and returns 1.
- FIFO order: for any sequence of pushes and pops starting from `rb_init`, the
  values returned by successful pops are the successfully pushed values in push
  order.
- `count` never exceeds `RB_CAPACITY` in any state reachable from `rb_init`.

### Caller obligations
- The invariant `count <= RB_CAPACITY && head < RB_CAPACITY` is established by
  `rb_init` and preserved by every function; callers must not modify the struct
  fields directly.
- All postconditions are stated conditionally on the function returning.

### External assumptions
None. `ring_buffer.c` calls no external functions.

For a verification task where a bug was found—suppose rb_push had instead computed the write index as size_t tail = rb->head + rb->count;—you will get a message like this:

## Memory-Safety Violation Found in `rb_push`

**`rb_push` is not memory safe** under the stated caller obligations. The write index
is computed as `size_t tail = rb->head + rb->count;` with no reduction modulo
`RB_CAPACITY`, so whenever `head + count >= RB_CAPACITY` the store `rb->data[tail] =
value` writes past the end of the `data` array, into `head` and `count` and beyond.

**Failing case:** call `rb_init`, push the values 1 through 8, pop once (so `head ==
1` and `count == 7`), then push the value 9. The store targets `rb->data[8]`, one
element past the end of `data[RB_CAPACITY]`. On the tested layout this overwrites the
low bytes of `rb->head`.

**Reproducer:** `sim/rb_push_counterexample.c` fixes these inputs and calls the
unmodified implementation. Build and run instructions are in the file's comments.
Compiled and run with `-fsanitize=undefined`, the run reports `runtime error: index 8
out of bounds for type 'uint32_t [8]'` on the store in `rb_push`, and the reproducer
prints `head == 9` afterwards, an index that is itself out of range for `data`.
AddressSanitizer alone does not flag this write, because it stays inside the
`ring_buffer` object.

### Other requested properties
- `rb_init`, `rb_pop`, `rb_size` — proved memory safe under the obligations stated in
  their entries in the Properties table.
- `rb_init` establishes `rb_size(rb) == 0` — proved.
- `rb_pop` returns 0 and modifies nothing when the buffer is empty — proved.
- Remaining functional properties of `rb_push` and `rb_pop`, the FIFO property, and
  the bound `rb_size(rb) <= RB_CAPACITY` — not verified; each depends on the
  `rb_push` behaviour shown to be broken above.

The results concern the sources as submitted. No source file was modified.

The reproducer is delivered next to your sources in the result archive. You can compile and run it locally, for example:

$ cc -fsanitize=undefined -g -I. sim/rb_push_counterexample.c ring_buffer.c -o rb_counterexample
$ ./rb_counterexample

A memory-safety violation is reported as a counterexample, a concrete failing execution, rather than as a formal proof that the property is false.

Specifying what to verify

Properties may be given in the prompt directly or in any text or Markdown file included in the project directory and referenced from the prompt. Write them in terms of your own functions, parameters and struct fields. Useful things to state explicitly:

• Which functions are the targets. By default Aristotle verifies the functions you name and every helper they reach in your sources, and reports each of them separately.
• Caller preconditions the code does not check itself: which pointers are non-null, how large the buffers behind them are, which strings are NUL-terminated, which integer arguments are in range, and which buffers must not overlap. If you leave these open, Aristotle will ask, or will state the minimal obligations it needed and report them as caller obligations.
• What "correct" means for functional properties. Memory safety needs no specification beyond the preconditions; functional correctness does.

Multi-file programs are supported. Put all .c and .h files under the project directory. Functions called across files within your sources are verified against a single shared specification so that the results compose.

External libraries

Your code will call functions you did not write. Aristotle treats them as follows:

• The C standard library (glibc). Contracts for the standard headers (string.h, stdio.h, stdlib.h, ctype.h, errno.h, unistd.h, time.h and many more) are built in and used automatically. Caller obligations they impose, such as a destination buffer being large enough for sprintf output, are proved at each call site or reported as obligations on your callers. A few contracts hold only under an assumption about the client program (for example that it never fcloses a standard stream); Aristotle reports such an assumption when your code depends on it.
• Other libraries. You choose, when asked, between verifying the library code itself (upload its source under the project directory) and relying on an agreed description of its behavior. An assumed contract is stated in plain terms in the summary, together with every function whose result depends on it. Assuming a library's behavior does not verify the library's implementation, and the summary says so.
• Callbacks your code passes to a library (for example a qsort comparator) remain part of the verification scope.

Current limitations

Aristotle's C verification has the following limitations.

Results are partial-correctness results

Memory-safety and functional-correctness proofs state what holds if a function returns. They do not establish termination, total correctness or that a function returns at all. Every postcondition in a summary should be read as conditional on the function returning. Freedom from memory leaks is proved only when you ask for it.

Bugs are reported as counterexamples, not as proofs of incorrectness

Aristotle can prove a C property, and it can exhibit a concrete failing execution, but it does not produce a formal proof that a C property is false. A property that Aristotle could neither prove nor refute with a confirmed counterexample is reported as unverified, with the reason. A failed proof attempt on its own is never reported as a bug.

Sources are verified exactly as submitted

Aristotle never edits your C to make it easier to analyze: it will not swap memcpy for memmove, inline a header, delete an attribute, or stub out a function. If a construct in your sources is not supported, the functions that reach it are dropped from the verification scope and named in the summary, and everything else is still verified. If an unsupported construct blocks every requested function, the run finishes with a report saying exactly what blocked it.

Verification artifacts are not returned

For C projects the deliverables are your submitted sources, the summary, the per-function entries in the project's Properties table, and any counterexample reproducers under sim/. If Aristotle claims it has verified a function, this is always based on a machine-checked formal proof of the property for a mechanically (not agentically) produced formal embedding of the function against a formal semantics of C on Linux/x86-64. However, the internal verification artifacts are not included in the result archive.

Assumptions

Aristotle uses a formal model of C on Linux/x86-64 (more specifically, gcc on Ubuntu 24.04) that follows the platform as documented, plus some known platform bugs. The model takes into account C's unspecified subexpression evaluation order and most sources of undefined behavior, including operating on values loaded from uninitialized memory, out-of-bounds pointer formation, violating C's effective types (a.k.a. strict aliasing) rules (except when -fno-strict-aliasing is specified), and data races. Known gaps in this model include the following:

• The C standard allows compilers to miscompile infinite loops that perform no I/O or synchronization; Aristotle assumes your compiler does not.
• Aristotle currently ignores the restrict keyword.
• Aristotle currently assumes that floating-point operations behave according to the IEEE 754 standard, with banker's rounding (round to nearest, ties to even). This is true only when compiling with the -ffp-contract=off flag.

Supported language and platform features

Aristotle supports most standard C language constructs, including threads, mutexes, C11 atomics (sequentially consistent only for now), function pointers, recursion, variadic functions, unions, bitfields, goto, and variable-length arrays. It also supports certain gcc extensions, including some inline assembly, and it has access to vetted specifications for a growing set of glibc functions. For functions it has no specification for, it will ask you what to assume.