# A Verified Generational GC for OCaml > Source: > Published: 2026-08-25 04:40:53+00:00 # A Verified Generational GC for OCaml - Author: Nik Swamy, with thanks to Sheera Shamsu, KC Sivaramakrishnan, and Lef Ioannidis It’s been a few months since I’ve posted something here, partly because the summer at MSR is always a buzz of activity with interns, and these days even more buzzy than usual with interns turbo-charged with agents. This week is [ICFP](https://icfp26.sigplan.org/) and I’m looking forward to presenting an experience report: [Proofs Promptly: Proof-Oriented Programming with Agents](https://dl.acm.org/doi/10.1145/3828709). The paper describes our experience with agents in February, around the time of the ICFP submission deadline. The intention of the paper was primarily to alert the programming languages research community to the step change in proving capability that we had seen with coding agents, though I think by now, most people interested in proofs have experienced this already. But, agentic proving is still very fresh and there are a lot of questions to explore, and this post describes my experience with a couple of them. The main question is about *proof maintenance*. Agents can write proofs, but can they work with large existing proof developments, maintain and evolve them as tools & requirements change? One of the examples in our *Proofs Promptly* paper tries to get at some aspects of this. We used agents to port a verified mark and sweep collector for OCaml done by [Sheera Shamsu in her PhD thesis](https://link.springer.com/article/10.1007/s10817-025-09721-0) to the latest version of [F* and Pulse](https://github.com/FStarLang/FStar), our separation logic proof-oriented language. “A mellow robotic camel in the style of a graphic novel”, generated by Microsoft 365 Copilot Our experience was that agents are very capable of a large proof maintenance task, i.e., porting a proof from one framework to another, upgrading a toolchain, etc. This has been notoriously hard to do in the past (cf. upgrading from Lean 3 to Lean 4; the lock-in to Low* and Z3 versions described in this paper on [Project Everest](https://dl.acm.org/doi/10.1145/3805702), etc.). So, getting agents to handle such upgrades is a welcome breakthrough. But, there’s more to proof maintenance than porting a development. Typically, one has to repeatedly revise the specification, code, and proofs as the project evolves and the requirements change. So, what this post is mostly about is how we started with a mark & sweep collector in Pulse, and evolved it in many steps into a generational garbage collector and integrated it with OCaml. Aside from proof maintenance, we were also interested in understanding how agents can help develop verified code with specifications that are inherently complex. Real software components have complex interfaces which require ~~messy~~ intricate specifications. A GC’s interface with a language runtime involves detailed heap shape invariants, and properties expected of various data structures internal to OCaml’s runtime system. Putting agents to work in this setting was illuminating, in various ways. Some takeaways: - With help from domain experts (i.e., Sheera and KC), we made a plan to stage the development into several phases, adding features and complexity in order. - Feature staging helps in auditing the results, judging progress, and was important for sustained development. - Pulse supports verifying low-level code with extraction to C, allowing one to easily integrate it within a larger system, in this case the OCaml runtime. - Auditing specifications is the main bottleneck, and it requires considerable expertise in formal specification and some domain knowledge. But, one needs to audit only the specification, not the code & proofs. - I find that reading specifications carefully and *writing*for myself what each part of the specification means is the most effective way to judge what was proven—writing it down forces one to think things through and understand in detail so that one can explain it to others. This is colored by my experience as a researcher, and is perhaps something that other researchers can relate to: you don’t understand the work until you write the paper. - Of course, other specification auditing tools are helpful, including [SPOTs](/blog/2026-04-16-spotting-specs). Interestingly, proofs of the SPOTs for our GC are many thousand lines long. At the end of the day, we have a verified generational GC for use with OCaml 4, representing about 2,000 lines of verified C code. The whole development is about 80,000 lines of F* and Pulse—this is about twice the size of Sheera’s original development, though this is quite a bit larger than it probably “ought” to be (agentic proofs can be very verbose). The top-level specification is a reachable sub-graph isomorphism between the heaps before and after a collection, stated in a few hundred lines of F*. Everything is available at [FStarLang/pulse-verified-gc](https://github.com/FStarLang/pulse-verified-gc). Before diving in, I should say that this work was mostly done in May 2026, so the agents have gotten even better since then. My setup is pretty simple. I use Copilot CLI with the F* [proof-copilot agent](https://github.com/FStarLang/proof-copilot). The agent contains various tips about using F*, Pulse, Z3, etc. You can install it in Copilot CLI with just this: Or in Claude Code: ## Staging the Development of a Verified Generational GC [Section titled “Staging the Development of a Verified Generational GC”](#staging-the-development-of-a-verified-generational-gc) Like any software project, building a proof-oriented program proceeds in stages, adding complexity gradually. Even with agents, planning the work in stages helps, especially so that one can understand how the development is progressing and whether what is proven makes sense. Whereas previously, one might plan out the development in several very small stages, with agents, one can progress rapidly through the stages in relatively large jumps. The main stages in our development are described below, and we arrived at this staging after a few discussions with KC and Sheera (especially when I was visiting IIT Madras and the new [FP Launchpad](https://fplaunchpad.org/) center there). For each stage, we provided a short prompt to the agent, roughly a paragraph in length, comparable to what is described here. Besides the initial prompt for each stage, I did spent a lot of time reading and critiquing specifications and asking the agents to improve them in various ways. All my input to the agents was only in natural language. At no stage did I provide any proof hints or write any code. The overall structure of the proof is to first develop purely functional implementations of each part of the algorithm, then prove that functional code satisfies various desirable properties, and finally to prove that the imperative Pulse code refines the functional implementation. The Pulse code can then be extracted to C and linked with the OCaml runtime. ### A Verified Allocator [Section titled “A Verified Allocator”](#a-verified-allocator) The GC we started from did not have a verified allocator. However, the invariants of the GC are closely intertwined with the invariants of the allocator. For example, the free list data structure that the allocator uses is maintained in the same heap and header words that the GC manipulates. Ensuring that the allocator and GC respect each other’s invariants is important, and is a next step noted in Shamsu et al.’s paper. So, this was the first step in our evolution: a verified first-fit, free-list allocator composed with the mark-and-sweep GC. The prompt to the agent was simply to add such an allocator. ### Free Object Coalescing [Section titled “Free Object Coalescing”](#free-object-coalescing) With the allocator specifications and proofs in place, we could start work on other improvements that involved the allocator, with confidence that we had guardrails to keep the work on track. We started with an improvement to the sweep phase. The sweep phase of the GC reclaims memory by placing objects that were not reachable during the mark phase on the allocator’s free list. Our initial sweep implementation did not coalesce adjacent free objects, which results in fragmentation. We had the agents implement a single-pass coalescing sweep, and by staging the verified allocator first, we were able to ensure that free-object coalescing maintained all the allocator’s invariants. ### A Bounded Mark Stack [Section titled “A Bounded Mark Stack”](#a-bounded-mark-stack) In parallel with free object coalescing, in another branch, we had agents work on improving the mark phase, and then agents merged the two lines of work. The mark phase of the collector is a depth-first traversal of the reachable objects in the heap, marking objects that have been reached but not yet fully processed gray and recording them in a mark stack. Shamsu et al.’s collector had an unrealistic assumption: it required the mark stack to be at least as big as the heap itself, and this allowed them to prove that the mark stack never overflows. Our next step was to relax this assumption. We added support for a bounded mark stack, where if during a traversal the mark stack becomes full, we mark objects gray but do not push them on the stack. When the traversal completes, we rescan the heap to find any remaining gray objects, and perform another mark phase with these gray objects as roots, and repeat the mark phase, and keep repeating until no gray objects remain. The proof is probably the trickiest part of the development, and involves showing that the repeated mark phase with the bounded mark stack is equivalent to a mark phase with an unbounded mark stack, and further, that the repeated mark actually terminates. ### A Generational GC [Section titled “A Generational GC”](#a-generational-gc) OCaml 4 uses a generational collector with separate minor and major heaps. The minor heap has its own simple bump-pointer allocator. At each minor collection, the minor heap is scanned and all reachable objects are promoted to the major heap by calling the free-list based major heap allocator. The algorithm used is a breadth-first traversal, a variant of [Cheney’s algorithm](https://en.wikipedia.org/wiki/Cheney%27s_algorithm). The minor heap is then reset. A major collection is a mark-and-sweep collection of the major heap, and a full generational collection does a minor collection and then a major collection. However, there are many subtleties beyond this simple description: I’ll mention just a few: - Pointer rewriting: Unlike the mark & sweep collector, the generational GC actually moves objects in the heap. So, references to the objects that were moved have to be updated. - Reachable subgraph isomorphism: Since objects are moved and mutated, the correctness criterion for a generational collector is quite different than Shamsu et al.’s mark & sweep specification. I suggested to the agent to prove that the reachable subgraphs before and after a collection are isomorphic (without describing how exactly to define it, though I then had to review it in detail). This was probably the most sophisticated input that I provided: being able to describe this and then being able to audit the resulting definitions requires at least some mathematical background. - Interfacing with OCaml’s runtime data structures: References to objects in the minor heap can be on the stack (as usual), but also in fields of major heap objects that point back to the minor heap. To find all such objects, one would need to scan the entire major heap, but this is very inefficient. Instead, OCaml maintains a “remembered set”, a data structure that records all fields in the major heap that contain minor heap pointers. Our GC interfaces with OCaml’s runtime by reading this remembered set to find all minor heap roots. ### Concrete Interoperability & Performance Optimization with OCaml [Section titled “Concrete Interoperability & Performance Optimization with OCaml”](#concrete-interoperability--performance-optimization-with-ocaml) As a final step, we had the agents integrate C code produced from the verified Pulse sources with the OCaml 4.14 bytecode runtime. The first integration resulted in more C glue code than I was willing to accept, and so it required several rounds of iteration with the agent to get to a reasonable interface. In hindsight, I have thought that it might have been better to set the C level interface first and then force the verified implementation to match it, though this would have required writing lots of unverified code at the start, which is also a problem. In the end, adjusting interfaces after the proof was done was also worked fine. We were also able to do several performance optimizations by benchmarking on the same set of microbenchmarks that Shamsu et al. use. Mainly since we have a better overall algorithm, our performance is significantly better, though still noticeably slower than stock OCaml 4.14. Of course, this is a very preliminary benchmarking result. | Benchmark | verified-gen mean (s) | stock OCaml mean (s) | Ratio | |---|---|---|---| `binarytrees` | 15.685 ± 0.048 | 12.322 ± 0.060 | 1.27x | `count_change` | 0.371 ± 0.007 | 0.197 ± 0.004 | 1.88x | `fannkuchredux` | 68.934 ± 0.598 | 68.152 ± 0.116 | 1.01x | `fasta` | 3.619 ± 0.020 | 2.546 ± 0.008 | 1.42x | `mandelbrot` | 2.869 ± 0.008 | 1.843 ± 0.009 | 1.56x | `nbodies` | 0.711 ± 0.014 | 0.303 ± 0.005 | 2.34x | `quicksort` | 7.987 ± 0.064 | 7.772 ± 0.055 | 1.03x | `spectralnorm` | 3.325 ± 0.009 | 2.166 ± 0.016 | 1.54x | There are several improvements we have planned, including notably the following: - Our GC still uses a fixed heap size, rather than growing the heap on demand. - Making our generational GC incremental is the main new algorithmic sophistication to add. With these two things, we expect to close most of the gap to OCaml 4.14, but OCaml 5 is another story—it uses a concurrent GC, which would be a different level of complexity to tackle; perhaps a story to share in the future. Even closing the performance gap, I expect there will be lots of interesting concerns to tackle before one would be willing to use an agentically authored & verified GC in a production OCaml setting, e.g., could developers not intimately familiar with F* and Pulse specifications maintain the code with agents only? ### Cleanup, Refactoring, Maintenance [Section titled “Cleanup, Refactoring, Maintenance”](#cleanup-refactoring-maintenance) Interspersed with the main development, we have also had agents do various mundane proof maintenance tasks. F*, Pulse, Z3, etc. also keep evolving, and we have repeatedly had our agents migrate the code to the latest version of our tools—this has been entirely automatic, and a far cry from our prior experience of manual tool upgrades. Agents also have a tendency to keep adding code rarely deleteing anything, so building up technical debt. We had agents author and use dependence scanning tools in F* to identify and then remove dead code, in the process removing nearly 25,000 lines of unnecessary definitions and lemmas in the system. Without such tools, we had less success in getting agents to reliably identify and delete dead code. ## What is Proven [Section titled “What is Proven”](#what-is-proven) The progress in agentic proving has been amazing: we can now generate verified code for non-trivial systems with just high-level interactions with an off-the-shelf coding agent. But, the process of producing such proofs is by no means fully automatic: apart from the staging process, a lot of my interaction with the agent is in auditing specifications, critiquing what was proven and asking the agent to strengthen the proof in various ways. Agent interactions for specification auditing involves careful study, with a solid understanding both of formal specifications, the notation of the proof assistant, and also some domain knowledge (e.g., how a generational GC works, and specifically how it works in OCaml). Let’s look at the top-level specification of our generational GC, reproduced verbatim here, including the comments. Right away, you can see that this is quite a detailed specification: real software is complicated. Understanding it all and confirming that it makes sense takes some doing, and I’ll try to explain some of it here. ### Parameters & Preconditions [Section titled “Parameters & Preconditions”](#parameters--preconditions) - `gh:gen_heap_t` : The argument`gh:gen_heap_t` is a triple`{minor; major; fp_ref}` representing the OCaml heap. It contains a minor heap (an array of bytes), a major heap (another array of bytes), and`fp_ref` points to the head of the free list. The precondition`is_gen_heap gh 'd 'b 's 'fp` (line 10) stats that these objects are a well-formed heap and`'d, 'b, 's, 'fp` are logical variables representing the contents of the heap:`'d` is the contents of the minor heap;`'b` is the high-water mark of the minor heap’s bump-pointer allocator;`'s` is the contents of the major heap; and`'fp` is the value of the free-list head. - `roots` and`nroots` : The roots array contains pointers (64-bit addresses) to objects in the heap, the set from which we begin scanning for live objects.`nroots` is the length of that array (line 24) and`'rs` is the logical variable representing the contents of the roots array (line 11). - `fwd_arr` : The forwarding array has length`UpdatePtrs.fwd_array_size` (line 25) (where`fwd_array_size` is the minor heap size in bytes divided by 8) and is initally zeroed out (line 26). The forwarding array will store the new addresses of objects that have been promoted from the minor heap to the major heap. - `queue` : This is an array used by Cheney’s breadth-first traversal algorithm to track the objects that have been promoted to the major heap, but whose fields have yet to be scanned. The type`larray U64.t Cheney.queue_size` constrains its size directly to be also be the size of the minor heap divided by 8. One stylistic criticism: other array lengths are specified as preconditions, whereas the length of the queue is constrained using a refinement type, but they mean the same thing. - `slots` and`nslots` : These arrays represent OCaml’s ref-table, or remembered set, which contains the addresses of all major heap object fields that point back to the minor heap. As explained earlier, these pointers are also part of the root set for the minor collection. The logical value of the`slots` is`'sl` (line 14) and (at lines 27–30) these are constrained as follows:- `ref_table_sound` states that every slot is really a field offset of a live major heap object - `ref_table_covers_minor_ptrs` states that every major object containing a minor heap pointer is listed in the slots - `slots_pairwise_distinct` says what one expects: there are no duplicates in the slots array - `remembered_targets_in_roots` states that every object pointed to by the slots is included in the root set, so that those objects get scanned and promoted. Note: we still need the remembered set, so that we know which fields to update in the major heap. - - `st:grey_stack` is the mark stack explained earlier, and its logical value is`'st` (line 15) and that the stack is well-formed according to the`is_grey_stack` predicate. - `gen_gc_stack_budget` (line 22) states that the grey stack is initially empty; the stack’s capacity is at least as large as the root set; and the capacity is non-zero. - `GenInv.collection_heap_shape minor_st 's 'fp` is the main precondition, and it states all the shape invariants of the OCaml heap. It’s too detailed to describe in full here, but its main components are as follows:- the major heap is well-formed, with all object sizes fitting the heap bounds, every pointer in the heap pointing to a valid object, etc., including such details as the handling of infix objects (OCaml’s representation for mutually recursive closures), no-scan tags, etc. - the free list is well-formed, terminating linked list, and all its objects are colored “blue”, a tag representing a free object. - there are no black or grey objects initially, and no non-blue object points to a blue object. - ### Result & Postconditions [Section titled “Result & Postconditions”](#result--postconditions) `gen_gc` is proven a total function, meaning it always returns a pair of a `fp:U64.t` , the pointer to the new head of the free list, and a boolean `ok` which indicates whether we ran out of memory when promoting objects from the minor to the major heap. The postconditions return ownership of all the data structures to the caller, and the main interesing guarantees are in the `pure` part. - `gen_gc_roots_post` (line 48) states that the roots array contains exactly the post-minor collection roots used by the major collection - `gen_gc_heap_shape_post` (line 49) states that the minor heap’s bump pointer is set back to zero and that the final heap is well formed - `gen_gc_reachable_subgraph_isomorphism_post` (line 50) is the main correctness criterion, stating that if`ok` is true, then the reachable subgraph from the root set in the initial state is isomorphic to the heap at the end, and that all the non-pointer fields of all objects are unchanged. - `gen_gc_unreachable_final_blue_post` (line 52) states that every object that remains in the final major heap but is not reachable from the final roots is blue, meaning that all the garbage has been collected. The error case is also specified, stating that `gen_gc` returns `not ok` only when we hit the out-of-memory case. ## Writing as an Audit Tool [Section titled “Writing as an Audit Tool”](#writing-as-an-audit-tool) Auditing specifications as complex as the one just shown is not easy. It took several iterations to get to the specification shown above, and while I’m sure it could be improved further, there does not seem to be much gratuitous complexity remaining. *Writing forces critical thinking:* My main process for auditing such a specification is to try to write down myself what I think each part of the spec means. To do that, I read a lot of the spec and its associated definitions. Of course, it’s very easy to have the agent write a detailed review document (the repository has one such document), and such documents are helpful, but they can also gloss over details. I find that writing one’s own analysis of the specification forces one to to understand the specification to the extent that one can explain it to others. To write this blog post, I had to revisit a specification I had last reviewed in May, and by writing things down, I noticed several problems with the specification that I had the agent fix. You can see these fixes in this [PR](https://github.com/FStarLang/pulse-verified-gc/pull/15). They include things like removing several preconditions that were unreasonably strong; cleaning up the main isomorphism postcondition to prove a single end-to-end result; and proving that the error case is sound, i.e., `gen_gc` returns `not ok` only when it runs out of memory. (These changes took the agent a few hours, while I did some yard work on a Sunday.) ## Small Proof-Oriented Tests (SPOTs) [Section titled “Small Proof-Oriented Tests (SPOTs)”](#small-proof-oriented-tests-spots) In a [previous post](/blog/2026-04-16-spotting-specs), we described an audit technique that involved having the agent write small test cases against a verified component, proving that the precondition is satisfiable, and that the postcondition is strong enough to *prove* that the expected outcome of the test. We called such tests “small proof-oriented tests” or SPOTs. We had agents write SPOTs against our verified GC (in [this file](https://github.com/FStarLang/pulse-verified-gc/blob/main/spot/GC.SPOT.ConcreteCallFull.fst#L163)), exercising the generational GC on a three-object heap. Object `C` in the major heap points to `A` in the minor heap through its first field, while object `B` is unreachable. It sets up the root array with `C` and `A` , with the slot table containing `C` ’s field that points to `A` , proves that it can satisfy `gen_gc` ’s preconditions, and that `gen_gc` ’s postconditions are strong enough to prove that `A` is promoted and `C` remains alive and points to the promoted `A` . This test provides some assurance that the specification of `gen_gc` is precise, and that its definitions are usable by a client to do a non-trivial proof. The proof is indeed non-trivial: the whole infrastructure for the SPOT is about 5,000 lines long, but its top-level statement is short and relatively easy to review, i.e., the test and its specification are small, the proof is not. ## Conclusions [Section titled “Conclusions”](#conclusions) A few remarks in parting: The promise of program proof is that it reduces what one has to trust about a piece of code to its specification. While agents have substantially lowered the bar for proof-oriented programming, one still needs domain expertise and some specification review skills to be productive. The agents will only keep getting better, but human understanding of agent outputs will remain a concern. Finding ways to better structure specifications, enable specification reuse, abstract classes of specifications, etc. are all important areas for further research. What’s also clear to me is that agentic proving is well beyond the realm of of benchmark problems. While benchmarks are useful, and help gauge the level of full automation that agents can provide, there is a lot more interesting work to do in structuring human/agent interactions, e.g., developing tools for orchestrations, or techniques that facilitate review & understanding. Finally: of course, we are not the first to verify garbage collectors: there’s a rich body of related work and agents are trained on it. Besides, our work builds directly on Shamsu et al.’s work on a mark & sweep GC for OCaml.