Introduction

As the cornerstone of information systems, system software — operating systems, compilers, virtual machines, databases, and the like — forms the foundation on which the entire digital society runs. When such software fails, the consequences are often catastrophic. In recent years, failures of every kind, from large-scale cloud outages to sudden operating-system crashes, have been all too common, inflicting severe economic losses and social disruption. Keeping system software safe and reliable is no longer a nice-to-have; it is a basic line of defense the digital age must hold.

Among the many means of assurance, type systems, static analysis, dynamic testing, and model checking each have their strengths, yet each covers only particular classes of problems and cannot rule out defects across the board. Formal proof offers a firmer guarantee: grounded in rigorous mathematical reasoning, it can prove that a program meets its specification in every scenario, eliminating defects at the implementation level. For instance, the formally proved microkernel seL4 has been deployed in high-assurance settings such as DARPA’s military autonomous helicopters and is widely regarded as a benchmark for secure operating systems; the formally proved C compiler CompCert exhibited no implementation errors under large-scale testing and has been adopted by aerospace companies such as Airbus for developing safety-critical flight-control software.

Unfortunately, formal proof remains a “technical luxury” that only a handful of experts can wield. The root cause is not a lack of proving power, but the divide between development and proof: take the ubiquitous C language — developers write code in an imperative style, yet the proof work must be carried out in proof assistants built on functional languages, such as Isabelle/HOL and Rocq (formerly Coq), which means switching languages, tools, and mindsets and building the proof from scratch. Take the seL4 kernel: a kernel implementation that took roughly two person-years to write required nearly twenty person-years for its formal proof — a proving cost ten times that of development. This disconnect between development and proof is precisely the fundamental obstacle that keeps formal proof from becoming widespread and from fitting into an ordinary programmer’s daily work.

We believe the way out of this predicament is not to make developers adapt to existing proof tools, but the opposite: to build formal-proving capability natively into a programming language developers already know. Development and verification then share the same language, the same environment, and the same workflow, fusing the two deeply. We call this idea unifying development and proof, and on that basis we have built C*, a systems programming language for verifying C programs.

This idea rests on a crucial observation: writing a program and constructing a proof are, in essence, the same activity. Inspired by the Curry–Howard correspondence, we observed that under the imperative programming paradigm exemplified by C, program code describes how the “program state” evolves step by step as statements execute, while a proof describes how the “proof state” — the lemmas already established and the goal currently to be proved — evolves step by step as reasoning proceeds. Since both are imperative calculi that revolve around state, we may well use the same C syntax to tightly couple implementation and proof in a single source file.

Existing program-verification tools cluster around two poles. At one pole are the prover-centric tools, exemplified by Isabelle/HOL (used by seL4), Rocq (used by CompCert), and frameworks such as VST and Iris. These offer tremendous expressive power, but come with a steep learning curve that only a few experts can master, and they still suffer from the divide between the development language and the proof language. At the other pole are the automation-centric tools, such as Dafny, Verus, Frama-C, VeriFast, and CN. These are easy to pick up, but their expressiveness and extensibility are limited: once a problem exceeds the reach of automated solvers such as SMT, the tool either fails or becomes hard to debug, or one must switch to a separate proof environment to carry on. Beyond these, languages such as F*, ATS, Idris, and Lean achieve a fusion of program and proof within the functional paradigm, yet do not fit the imperative style that predominates in systems-software practice. C* takes the best of both poles: it retains C’s imperative paradigm, integrates full proving capability directly at the language level (not merely automated solving), and adds real-time feedback and debuggable specifications — pursuing both the expressiveness of proof and the ease of development.

To give an intuitive sense of C*, we take the classic example of reversing a singly linked list in place, implemented in C. Let us first review its implementation:

struct list {
  int head;
  struct list *tail;
};
struct list *reverse(struct list *pt) {
  struct list *ret = NULL;
  while (pt) {
    struct list *nxt = pt->tail;  // save the successor
    pt->tail = ret;               // reverse the link
    ret = pt;                     // advance the reversed prefix
    pt = nxt;                     // advance the remaining part
  }
  return ret;
}

struct list {
  int head;
  struct list *tail;
};
struct list *reverse(struct list *pt) {
  struct list *ret = NULL;
  while (pt) {
    struct list *nxt = pt->tail;  // save the successor
    pt->tail = ret;               // reverse the link
    ret = pt;                     // advance the reversed prefix
    pt = nxt;                     // advance the remaining part
  }
  return ret;
}

Simple as this program is, to prove it correct — that the return value really is the reversal of the input list — one must precisely characterize how each step changes memory. In C*, the specification and proof are not written elsewhere but embedded directly in the same C source, and both may be written in C syntax (for example, function-call expressions):

struct list *reverse(struct list *pt)
  [[cst::param(mk_var("l", mk_list_type(mk_int_type())))]]
  // ghost parameter: the list's logical contents l
  [[cst::require(`sll pt l`)]]
  // precondition: pt points to a list with contents l
  [[cst::ensure(`sll __return (REVERSE l)`)]]
  // postcondition: the return value points to a list with contents REVERSE l
{
  struct list *ret = 0;
  [[cst::proof]] fold_sll_null(`0i`);            // a null pointer is the empty list
  while (pt)
    [[cst::invariant(`exists l1 l2 pt_v ret_v.
        fact(l == REVERSE l1 ++ l2) **
        data_at pt__addr Tptr pt_v ** data_at ret__addr Tptr ret_v **
        sll ret_v l1 ** sll pt_v l2`)]]
  {
    [[cst::proof]] unfold_sll_not_null(`pt_v`);  // open the list head to obtain ownership of tail
    struct list *nxt = pt->tail;
    pt->tail = ret; ret = pt; pt = nxt;
    [[cst::proof]] fold_sll_not_null(`pt_v`);    // fold back the list on the ret side
    [[cst::proof]] assert_by_rewrite(            // use list theory to prove the invariant is maintained
      `l == REVERSE (h :: l1) ++ t`,
      ThmList(REVERSE_DEF, APPEND_DEF)
    );
  }
  return ret;
}

struct list *reverse(struct list *pt)
  [[cst::param(mk_var("l", mk_list_type(mk_int_type())))]]
  // ghost parameter: the list's logical contents l
  [[cst::require(`sll pt l`)]]
  // precondition: pt points to a list with contents l
  [[cst::ensure(`sll __return (REVERSE l)`)]]
  // postcondition: the return value points to a list with contents REVERSE l
{
  struct list *ret = 0;
  [[cst::proof]] fold_sll_null(`0i`);            // a null pointer is the empty list
  while (pt)
    [[cst::invariant(`exists l1 l2 pt_v ret_v.
        fact(l == REVERSE l1 ++ l2) **
        data_at pt__addr Tptr pt_v ** data_at ret__addr Tptr ret_v **
        sll ret_v l1 ** sll pt_v l2`)]]
  {
    [[cst::proof]] unfold_sll_not_null(`pt_v`);  // open the list head to obtain ownership of tail
    struct list *nxt = pt->tail;
    pt->tail = ret; ret = pt; pt = nxt;
    [[cst::proof]] fold_sll_not_null(`pt_v`);    // fold back the list on the ret side
    [[cst::proof]] assert_by_rewrite(            // use list theory to prove the invariant is maintained
      `l == REVERSE (h :: l1) ++ t`,
      ThmList(REVERSE_DEF, APPEND_DEF)
    );
  }
  return ret;
}

In C*, proofs of a program’s safety and correctness are carried out in separation logic — a logic well suited to describing pointers and memory ownership. Syntactically, the backtick form `...``...` encloses logical assertions: sll pt lsll pt l reads as “pointer ptpt points to a singly linked list with contents ll”, **** (separating conjunction) joins two disjoint regions of memory, data_at a Tptr vdata_at a Tptr v means address aa holds the pointer value vv, REVERSEREVERSE and ++++ are logical functions (reverse and append) reused directly from an existing list theory, __return__return denotes the return value, and __addr__addr denotes the address of variable . Around these, C* provides three kinds of annotations: [[cst::require(...)]][[cst::require(...)]] / [[cst::ensure(...)]][[cst::ensure(...)]] (together with the ghost parameter [[cst::param(...)]][[cst::param(...)]]) declare a function contract, [[cst::invariant(...)]][[cst::invariant(...)]] declares a loop invariant, and [[cst::proof]] ...[[cst::proof]] ... embeds proof code within the program. For example, unfold_sll_not_nullunfold_sll_not_null in the loop body (a C* function) opens the head node of a non-empty list to obtain ownership of the tailtail field explicitly, so the subsequent read/write of pt->tailpt->tail becomes legal; assert_by_rewriteassert_by_rewrite (another C* function) uses the equational laws of list theory to prove the invariant is maintained across the loop. The C* functions above — including mk_varmk_var, mk_list_typemk_list_type, and mk_int_typemk_int_type used in the contract — are themselves ordinary C code, so one can practice proof engineering on them just as in software engineering, for instance by building reusable proof libraries.

In the C* programming environment, development and proof are synchronous and real-time. For example, when you reach the entry of the loop body, the environment can display the symbolic state at that point in real time:

It gives the program’s precise symbolic state at this moment: there exist a reversed prefix l1l1 and a remaining part l2l2 such that l == REVERSE l1 ++ l2l == REVERSE l1 ++ l2; retret points to a list holding contents l1l1, ptpt points to a list holding contents l2l2, and the two are disjoint. With every line of code you write, this symbolic state updates accordingly; if a step lacks the required ownership, C* reports an error in real time — for example, accessing pt->tailpt->tail without first unfoldunfolding it yields “cannot derive the precondition for the memory access”. After you finish a function, if a proof of the loop invariant or the postcondition is missing, C* reports the outstanding verification conditions at the corresponding places.

C* not only achieves a deep fusion of development and proof at the level of the programming language, the programming environment, and the workflow, but also opens up the following two new research directions.

First, programmable verification automation. We are rethinking the architecture of the “program verifier” from the perspective of a “theorem prover” architecture: turning the various automation tactics used during verification into reusable, composable proof libraries that developers extend as needed, without having to place these tactics in the trusted computing base. This idea extends equally to program analysis: writing specification annotations such as assertions and loop invariants is the most tedious part of verification. To address this, we can implement mature program-analysis techniques — pointer alias analysis, invariant inference, and the like — as the same kind of proof libraries, coupling them tightly with the verification workflow to generate specification annotations automatically and lighten the manual burden. More importantly, the analysis results can be checked by the proof kernel; since the analysis modules need not be in the trusted computing base, even a buggy analyzer cannot produce a false proof. This fuses program analysis, type systems, and the like with formal proof, enjoying the convenience of automated tools without sacrificing trustworthiness.

Second, agent-oriented trustworthy programming. Large language models are transforming software development, but the question of whether AI-written code is actually correct remains unresolved. Combining large models with formal proof — using large models to bring down the high cost of formal proof, and using formal proof to give safety guarantees for the programs large models write — has become a shared goal of academia and industry. Compared with existing formal-proof languages, C* is a better fit for large models: (1) large models are error-prone when jumping around and reading many files, whereas C*‘s design keeps program and proof in one place, requiring no extensive jumping to complete a task, making it more suitable for large models than languages that separate development from proof; (2) SMT-based languages often give only weak feedback and behave unstably across repeated runs, whereas C* maintains a unified, stable symbolic state for both proofs and ordinary C statements, better guiding a large model to write and revise code and avoiding getting stuck when errors occur. Spanning data, training, and environment design, we are building exactly such an agent for C* — one that writes both code and proofs.

These explorations all ultimately point toward bringing formal proof into industrial practice: applying C* to the verification of systems software such as operating-system kernels and network-protocol implementations, and accumulating reusable, high-assurance code libraries; and lowering the barrier to teaching program verification — from requiring doctoral-level expertise down to something undergraduates can reach — so that far more people can genuinely put formal proof to use.