Is it possible to build a formally verified GC for OCaml that can be plugged into the compiler? We should how to in: "A Mechanically Verified GC for OCaml" kcsrk.info/papers/verif... This has been accepted to the Journal of Automated Reasoning. Code: github.com/prismlab/ver... - ThreadSky

kcsrk.info • 2 days ago

Is it possible to build a formally verified GC for OCaml that can be plugged into the compiler? We should how to in:

"A Mechanically Verified GC for OCaml"

https://kcsrk.info/papers/verifiedgc_feb_25.pdf

This has been accepted to the Journal of Automated Reasoning.

Code: https://github.com/prismlab/verified_ocaml_gc

Comments

shreyascodes.tech•2 days ago

📌

shoebum.bsky.social•1 day ago

Wow this is huge 🌴🐫🌴

patrick.sirref.org•2 days ago

That's awesome, congratulations!

I saw last week that we just got an FStar on opam that will work with OCaml 5+ https://github.com/ocaml/opam-repository/pull/27476 :))

kcsrk.info•2 days ago

Yes. Pretty cool. https://discuss.ocaml.org/t/ann-new-f-release-on-opam-2025-02-17/16179

If we can get Pulse to target concurrent/parallel OCaml, we’d be able to prove and generate verified concurrent OCaml code.

I believe this would be the complement of all the cases DRFcaml wouldn’t cover such as lockfree concurrent programs(?).

kcsrk.info•2 days ago

The GC is simple -- a stop-the-world mark-and-sweep, non-generational, non-incremental, not concurrent or parallel. No support for weak references, ephemerons, finalisers.

That said, we prove it correct and support enough features (closures, infix objs) to be able to run reasonably big programs.

kcsrk.info•2 days ago

Our language of choice is F* where we describe describe the GC correctness spec, implement the GC model and show that the implementation model matches the spec. Finally, implement the GC in Low*, a subset of F* that can be extracted to memory-error free C, and show that Low* impl matches the model.

kcsrk.info•2 days ago

Low* code is extracted to C using Karamel compiler. A key achievement is that there no "air gap" between what we verify and what we execute.

kcsrk.info•2 days ago

It has been challenging to get this paper out to the world as it falls between GC land (reviews -- GC is too simple) and verification land (reviews -- verification is uninteresting). The earlier drafts were rejected many times (some of them definitely warranted), but happy to get this out finally.

kcsrk.info•2 days ago

Our simple verified GC, though spartan, is already useful in domains where latency is not a problem but correctness is -- proof checkers, verified compilers, etc. A verified GC reduces the TCB of OCaml.

kcsrk.info•2 days ago

There's certainly lots of interesting future work to be done here -- make it incremental, generational, concurrent, parallel, integrate a verified allocator (https://dl.acm.org/doi/10.1145/3689773), support missing features.

kirancodes.me•2 days ago

kinda orthogonal question if that's okay, did you run into like issues with the verification times using F*? I see from the paper that the full GC verification times took 0.5/2 hours.

Did you run into like issues with slow proofs or did you have to rewrite things for efficiency at any point>

kcsrk.info•2 days ago

Using F* SMT-aided proof is quite a challenge. More than the running times, it is the proof stability that's been quite challenging. Z3 is quite temperamental and even with the exact version, any change in the environment (different OS), may make the proofs unstable.

kirancodes.me•2 days ago

oooh this paper is super cool! I love seeing like formal verification proof-engineering related stuff (w.r.t like architecting the proof such that it could be plugged in)!

jack.quartztz.com•2 days ago

been very interested in F* lately, so glad to see it used in such a cool project. amazing paper!

legcop.bsky.social•1 day ago

That's an interesting research paper, it seems like a significant achievement in formal verification for programming languages.

thomega.bsky.social•2 days ago

s/should/showed/

Comments

Posting Rules

Reply