Pith. sign in

REVIEW 2 major objections 6 minor 41 references

A complete concurrent incorrectness logic for OCaml lets LLMs attach machine-checked proofs that reported bugs are real, so false alarms can be rejected.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-14 04:23 UTC pith:YM6PTAE7

load-bearing objection Solid, mechanized complete concurrent incorrectness logic for OCaml/ZooLang; the agentic angle is honest PoC, not the load-bearing claim. the 2 major comments →

arxiv 2607.11611 v1 pith:YM6PTAE7 submitted 2026-07-13 cs.PL

Mizzle: A Complete Concurrent Incorrectness Logic for Preventing False Alarms in Agentic Bug Finding

Alexandre Moine , Sam Westrick , Joseph Tassarotti This is my paper
classification cs.PL
keywords incorrectness logicseparation logicconcurrent OCamlLLM bug findingfalse alarmslinearizabilitydata racesprogram verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Large language models already find subtle bugs, but they also drown developers in false alarms that are hard to dismiss. This paper proposes that every LLM bug report must come with a machine-checked proof, written in an incorrectness program logic, that the claimed bad behavior is genuinely reachable. The authors build Mizzle, a concurrent incorrectness separation logic for a substantial subset of OCaml 5, parametric in the chosen notion of incorrectness, mechanized in Rocq on Iris, and proved both sound (it never certifies a false alarm) and complete (every incorrect execution has a derivation). They instantiate it for stuckness, non-linearizability of concurrent data structures, and memory races, and show as a proof of concept that an LLM can drive Mizzle to certify concrete bugs. A sympathetic reader cares because the method turns agentic bug finding from an untrustworthy flood of reports into a pipeline in which every accepted report is a true positive that a proof assistant has checked.

Core claim

Mizzle is a concurrent incorrectness separation logic for ZooLang (a model of concurrent OCaml 5) that is parametric in the incorrectness predicate. Mechanized in Rocq, it is sound: a derivation of goal from remaining(witness P) implies a reachable configuration satisfying P. It is also complete: every reachable incorrect configuration admits a Mizzle derivation under mild location-freedom assumptions. Instantiated for stuckness, non-linearizability, and races, it lets an LLM produce a machine-checked certificate that a reported bug is real.

What carries the argument

Mizzle: an angelic, goal-oriented concurrent incorrectness separation logic whose remaining and witness assertions force the user to exhibit a reachable incorrect configuration; the soundness and completeness theorems (4.1–4.2 and their corollaries) guarantee that checked proofs cannot be false alarms and that no real bug is ruled out for want of a derivation.

Load-bearing premise

Completeness only holds when the program, and for non-linearizability the emitted history, contain no hard-coded memory locations, because the logic treats locations abstractly via renaming.

What would settle it

Exhibit a location-free program that reaches a stuck, non-linearizable, or racy configuration for which no Mizzle derivation exists, or produce a checked Mizzle derivation of goal for a program that has no execution satisfying the claimed incorrectness predicate.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Any LLM bug report accompanied by a checked Mizzle derivation is guaranteed to be a true positive.
  • No real stuck, non-linearizable, or racy execution in the supported OCaml fragment is excluded merely because the logic cannot express it.
  • Developers can demand machine-checked certificates instead of multi-model review or flaky schedule-dependent tests for concurrency bugs.
  • Axiomatic library specs (for example parallel-for) let proofs focus on client bugs without stepping into library internals.
  • A total weakest-precondition correctness proof of a component can be reused inside Mizzle to advance threads while hunting client bugs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same certificate pipeline could be required of other agentic or automated bug finders that currently lack a machine-checked under-approximation guarantee.
  • The mirror assertion used for completeness offers a reusable pattern for proving completeness of other under-approximate Iris logics without fixing concrete allocation addresses.
  • If tactic support and prompting improve, the multi-dollar-per-case cost shown in the evaluation could fall low enough for continuous integration of LLM-found concurrency bugs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper introduces Mizzle, a concurrent incorrectness separation logic for a substantial subset of OCaml 5 (ZooLang), parametric in the incorrectness predicate. Mizzle is mechanized in Rocq on Iris and proved sound (a derivation of goal from remaining(witness P) yields a reachable configuration satisfying P) and complete (every reachable incorrect configuration admits a derivation, under mild location-freedom assumptions). It is instantiated for stuckness, non-linearizability (via a most-general client and trace events), and races. A proof-of-concept evaluation shows Claude Sonnet 5 can construct machine-checked Mizzle proofs for hand-bugged concurrent data structures and DataRaceBench-style race examples, with openly acknowledged tuning and framing biases.

Significance. If the mechanized claims hold, this is a substantial contribution: the first concurrent incorrectness logic that is both complete and mechanized for a realistic concurrent language fragment, with three nontrivial incorrectness notions including direct non-linearizability rather than an encoding as stuckness. The machine-checked soundness and completeness theorems (Theorems 4.1–4.2, Corollaries 2.1–2.4), the Iris embedding, and the parametric witness/remaining/goal design are genuine strengths. The LLM evaluation is correctly scoped as a cost-of-proof PoC rather than a claim about improved bug finding, which keeps the formal contribution cleanly separated from the agentic application.

major comments (2)
  1. §5.3 and §7: the axiomatized parallel_for specification spawns n independent iterations and is used in the race case studies. The paper correctly notes that invalid axioms can introduce unrealizable behaviors and thus false alarms relative to a concrete library. Because the central application is preventing false alarms, the manuscript should state more sharply which evaluation results are relative to the axiom versus relative to domainslib’s actual chunking semantics, and whether any reported race is known to be unrealizable under the real library. Without that, the PoC’s claim to “certify the existence of a bug” is ambiguous for the race suite.
  2. §4.4, Theorem 4.2 and Corollary 2.4: completeness for non-linearizability requires that the emitted history contain no locations (so that the mirror renaming acts as the identity on the trace). The most-general-client construction can emit abstract tags/values, but realistic data structures often store and return locations. The paper should either (a) show how to lift NonLinearizable through the renaming bijection when histories mention locations, or (b) state clearly that completeness for non-linearizability is limited to location-free abstract models and does not cover histories that mention heap addresses. This is load-bearing for the “every incorrect execution admits a derivation” slogan as applied to non-linearizability.
minor comments (6)
  1. §2.3 / Fig. 2: the continuation-passing style (remaining on the left, goal on the right) is clear once explained, but a short side-by-side comparison with a classical under-approximate triple would help readers coming from ISL/CISL.
  2. §3.1: the list of differences with full ZooLang is useful; a one-line statement that soundness/completeness are proved against the full mechanized language (as claimed later) would reduce the risk that readers think the paper only covers the subset shown.
  3. §5.1: “Claude Sonnet 5” should be checked against the actual model name used; also fix the typo “potentailly” in the framing-bias paragraph.
  4. Fig. 14–15: reporting average MCP failure rates is informative; adding a column for proof lines (already mentioned in text) would make the tables self-contained.
  5. Related work (§6): the comparison with CASL on data-dependent bugs is good; a sentence on whether Mizzle’s angelic interleaving style can encode CASL-style adversarial clients would strengthen the positioning.
  6. References: several 2026 citations (Zoo, Angelic, Soteria, etc.) are contemporaneous; ensure final versions or DOIs are updated if available at camera-ready.

Circularity Check

0 steps flagged

No significant circularity: soundness and completeness are proved relative to an independent operational semantics of ZooLang, with no fitted parameters, self-definitional reductions, or load-bearing self-citation chains.

full rationale

The central claims (Theorems 4.1–4.2 and Corollaries 2.1–2.4) establish that a Mizzle derivation of goal from remaining(witness P) yields a reachable configuration satisfying P (soundness), and conversely that every reachable incorrect configuration admits a derivation under mild location-freedom assumptions (completeness). These are proved by induction on the operational semantics of ZooLang (Figures 5–6) and the definition of goal as a least fixpoint (Figure 13), using the standard Iris state-interpretation relation (Figure 8) and the mirror assertion for renaming (Figure 12). Stuck, NonLinearizable and Racy are defined independently of the logic (Figures 9–11) from the same semantics; witness P simply packages them. Self-citations (Iris, ZooLang, Angelic) supply background infrastructure or stylistic inspiration for the goal assertion; none is invoked as an unverified uniqueness theorem or ansatz that forces the result. There are no empirical fits, no predictions that reduce to inputs by construction, and no renaming of a known pattern. The location-freedom caveats of completeness are explicit scope restrictions, not circular reductions. The LLM evaluation is a separate proof-of-concept and does not underwrite the formal theorems. The derivation chain is therefore self-contained against the operational model.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 2 invented entities

The paper is a formal-logic development. Its load-bearing background is the operational semantics of ZooLang (itself a model of OCaml 5), the Iris framework, and standard definitions of linearizability and races. No free parameters are fitted. The only ad-hoc elements are the axiomatized parallel_for used in the race case studies and the decision to treat all accesses as potentially racy.

axioms (4)
  • domain assumption ZooLang small-step interleaving semantics accurately models the concurrency and physical-equality behavior of OCaml 5 domains (Allain & Scherer 2026).
    All soundness and completeness statements are relative to this model (§3).
  • standard math Iris separation-logic framework and its ghost-update modality are sound.
    Mizzle is embedded on top of Iris; goal is defined via a least fixpoint using Iris updates (§4.5).
  • ad hoc to paper The axiomatized parallel_for specification (spawning n independent iterations) is a valid under-approximation for bug finding even when the real library chunks work.
    Used in the DataRaceBench case studies (§5.3); the authors note it does not hold for the concrete chunking implementation.
  • standard math Linearizability is defined via the existence of a linearization-event enrichment that is sound w.r.t. a sequential model (standard Herlihy–Wing style).
    Used for the NonLinearizable predicate (§4.2, Fig. 10).
invented entities (2)
  • Mizzle goal / remaining / witness assertions (continuation-passing incorrectness judgments) no independent evidence
    purpose: Encode under-approximate reachability proofs in a form that an LLM can discharge step-by-step inside Rocq.
    These are the core proof-theoretic objects of the logic; they have no independent existence outside the paper.
  • mirror assertion (location-renaming bijection between operational configurations and separation-logic resources) no independent evidence
    purpose: State completeness in the presence of allocation nondeterminism.
    Technical device needed because Mizzle quantifies universally over fresh locations (§4.4).

pith-pipeline@v1.1.0-grok45 · 34960 in / 2806 out tokens · 30487 ms · 2026-07-14T04:23:56.853389+00:00 · methodology

0 comments
read the original abstract

Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers' time. We propose a method to prevent these false alarms by requiring an LLM to accompany each bug report with a machine-checked proof, in a program logic, that the reported bug is real. We follow the approach of incorrectness logics, whose under-approximate reasoning establishes that a claimed behavior is genuinely reachable, and hence a true positive. In our case, however, the logic must model a realistic programming language, have a mechanization so that proofs can be checked, and be complete, so that no real bug is ruled out for want of a derivation. We present Mizzle, an incorrectness separation logic for concurrent programs written in a substantial subset of OCaml, parametric in the notion of incorrectness. We mechanize Mizzle in the Rocq proof assistant on top of the Iris framework, and we prove that it is both sound (that is, it never justifies a false alarm) and complete (that is, every incorrect execution admits a derivation). We instantiate Mizzle with three notions of incorrectness: stuckness (triggering undefined behavior), the non-linearizability of a data structure, and the presence of a race. As a proof of concept, we illustrate how an LLM can use Mizzle in order to certify the existence of a bug.

Figures

Figures reproduced from arXiv: 2607.11611 by Alexandre Moine, Joseph Tassarotti, Sam Westrick.

Figure 1
Figure 1. Figure 1: A buggy concurrent stack Scherer 2026] as a formal operational model of OCaml 5 (§ 2.2). Next, we present the key rules of Mizzle and explain how to prove the existence of the bug by showing a stuck configuration is reachable (§2.3). Mizzle is in fact parameterized by the notion of incorrectness being looked for, and stuckness is just one instantiation. We illustrate this generality with a second instantia… view at source ↗
Figure 2
Figure 2. Figure 2: Key reasoning rules of Mizzle: the assert function, the remaining assertion, forks, and compare-and-set [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Reasoning rules for non-linearizable traces [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The most general client The function most_general_client takes three arguments: init, initializing the data structure, op, applying an operation on the data structure, and gen, generating arguments for the operation. The most_general_client initializes the data structure, then repeatedly non-deterministically spawns threads. Each thread runs one function call, emitting a Call event before the call and a Re… view at source ↗
Figure 5
Figure 5. Figure 5: Syntax of ZooLang fields 𝑣®. Mutable blocks are instead heap-allocated and denoted by their location ℓ. Constructor tags allow distinguishing between different constructors of an algebraic data type. For example, in the case of the type option in OCaml, the data None is represented by the block ⟨0 |⟩, while the data Some v is represented by the block ⟨1 | 𝑣⟩. The Rocq implementation of ZooLang offers notat… view at source ↗
Figure 6
Figure 6. Figure 6: Selected rules of the semantics omit generativity, a mechanism that gives immutable blocks an observable identity. Second, ZooLang functions are in fact mutually recursive bundles together with a selector index; we ignore this aspect. Third, the match construct of ZooLang additionally features a default branch, binding the scrutinee, which we elide. Fourth, we omit the atomic operations Xchg (exchange) and… view at source ↗
Figure 7
Figure 7. Figure 7: Reasoning rules for block construction, allocation, loads, and stores [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Reasoning rules for the interp predicate [PITH_FULL_IMAGE:figures/full_fig_p014_8.png] view at source ↗
Figure 10
Figure 10. Figure 10: Linearizability as a trace property Non-Linearizability [PITH_FULL_IMAGE:figures/full_fig_p015_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The LAcc and Acc access predicates, and the Racy predicate [PITH_FULL_IMAGE:figures/full_fig_p016_11.png] view at source ↗
Figure 13
Figure 13. Figure 13: Definition of the 𝔤𝔬𝔞𝔩 assertion one witnessing Racy𝑐, while the in-bounds requirement on the two accesses corresponds to an invariant of the reduction relation. Lemma 4.5. If𝑐 has two distinct threads 𝜋1 ≠ 𝜋2 executing expressions 𝑒1 and 𝑒2 such that LAcc 𝑒1 ℓ 𝑏1 and LAcc 𝑒2 ℓ 𝑏2 hold for the same location ℓ with 𝑏1 ∨ 𝑏2, and both accesses are in bounds, then mirror𝑐 ⊢ witness Racy. 4.5 Inside the Goal A… view at source ↗
Figure 14
Figure 14. Figure 14: Evaluation of Mizzle being used by Claude Sonnet 5 to prove non-linearizability. The minimum [PITH_FULL_IMAGE:figures/full_fig_p020_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Evaluation of Mizzle being used by Claude Sonnet 5 to prove the existence of a memory race. The [PITH_FULL_IMAGE:figures/full_fig_p021_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: One representative from each bug family: a shared cell, a loop-carried dependence, and an indirect [PITH_FULL_IMAGE:figures/full_fig_p022_16.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 12 canonical work pages

  1. [1]

    Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic.Proceedings of the ACM on Programming Languages10, POPL (Jan. 2026). doi:10.1145/3776701 Anon

    work page doi:10.1145/3776701 2026

  2. [2]

    ACM Program

    Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!Proc. ACM Program. Lang.10, PLDI, Article 228 (June 2026), 26 pages. doi:10.1145/3808306 Sacha-Élie Ayoun. 2025.Gillian: Foundations, Implementation, and Applications of Compositional Symbolic Execution. Ph. D. Dissertation. Imperial ...

    work page doi:10.1145/3808306 2026

  3. [3]

    arXiv:2601.05385 [cs.SE] https://arxiv.org/abs/2601.05385 Jonas Bayer, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Michael Tautschnig, and Soonho Kong

    DafnyPro: LLM-Assisted Automated Verification for Dafny Programs. arXiv:2601.05385 [cs.SE] https://arxiv.org/abs/2601.05385 Jonas Bayer, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Michael Tautschnig, and Soonho Kong

    arXiv

  4. [4]

    arXiv:2605.06184 [cs.SE] https://arxiv.org/abs/2605.06184 Sam Blackshear, Nikos Gorogiannis, Peter W

    Teaching LLMs Program Semantics via Symbolic Execution Traces. arXiv:2605.06184 [cs.SE] https://arxiv.org/abs/2605.06184 Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey

    Pith/arXiv arXiv

  5. [5]

    RacerD: compositional static race detection. Proc. ACM Program. Lang.2, OOPSLA, Article 144 (Oct. 2018), 28 pages. doi:10.1145/3276514 James Brotherston, Paul Brunet, Nikos Gorogiannis, and Max Kanovich

    doi:10.1145/3276514 2018

  6. [6]

    In2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)

    A Compositional Deadlock Detector for Android Java. In2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). 955–966. doi:10.1109/ASE51524.2021.9678572 Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan

    doi:10.1109/ase51524.2021.9678572 2021

  7. [7]

    InProceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10,

    Line-up: a complete and automatic linearizability checker. InProceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10,

    2010

  8. [8]

    doi:10.1145/1806596.1806634 Cristiano Calcagno, Dino Distefano, and Peter O’Hearn

    ACM, 330–340. doi:10.1145/1806596.1806634 Cristiano Calcagno, Dino Distefano, and Peter O’Hearn

    work page doi:10.1145/1806596.1806634

  9. [9]

    https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/

    Open-sourcing Facebook Infer: Identify bugs before you ship. https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/. Edsko de Vries and Vasileios Koutavas

    arXiv

  10. [10]

    Accessed: 2026-07-05

    https://github.com/ocaml- multicore/domainslib. Accessed: 2026-07-05. Brijesh Dongol and John Derrick

    2026

  11. [11]

    Surv.48, 2 (2015), 19:1–19:43

    Verifying Linearisability: A Comparative Survey.ACM Comput. Surv.48, 2 (2015), 19:1–19:43. doi:10.1145/2796550 Michael Emmi and Constantin Enea

    work page doi:10.1145/2796550 2015

  12. [12]

    ACM Program

    Sound, complete, and tractable linearizability monitoring for concurrent collections.Proc. ACM Program. Lang.2, POPL (2018), 25:1–25:27. doi:10.1145/3158113 Mingdong Feng and Charles E. Leiserson

    doi:10.1145/3158113 2018

  13. [13]

    InProceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures(Newport, Rhode Island, USA)(SPAA ’97)

    Efficient detection of determinacy races in Cilk programs. InProceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures(Newport, Rhode Island, USA)(SPAA ’97). Association for Computing Machinery, New York, NY, USA, 1–11. doi:10.1145/258492.258493 José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner

    work page doi:10.1145/258492.258493

  14. [14]

    InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020)

    Gillian, part i: a multi-language platform for symbolic execution. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing Machinery, New York, NY, USA, 927–942. doi:10.1145/3385412.3386014 Maurice P. Herlihy and Jeannette M. Wing

    doi:10.1145/3385412.3386014 2020

  15. [15]

    https://doi.org/10.1145/78969.78972 Alex Horn and Daniel Kroening

    Linearizability: a correctness condition for concurrent objects.ACM Transactions on Programming Languages and Systems12, 3 (July 1990), 463–492. https://doi.org/10.1145/78969.78972 Alex Horn and Daniel Kroening

    doi:10.1145/78969.78972 1990

  16. [16]

    Faster Linearizability Checking via P-Compositionality. InFormal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, Mizzle: A Complete Concurrent Incor...

    work page doi:10.1007/978-3-319-19195-9_4 2015

  17. [17]

    doi:10.1038/s41586-025-09833-y C

    Olympiad-level formal mathematical reasoning with reinforcement learning.Nature651, 8106 (2025), 607–613. doi:10.1038/s41586-025-09833-y C. B. Jones

    doi:10.1038/s41586-025-09833-y 2025

  18. [18]

    Tentative steps toward a development method for interfering programs.ACM Trans. Program. Lang. Syst. 5, 4 (Oct. 1983), 596–619. doi:10.1145/69575.69577 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer

    doi:10.1145/69575.69577 1983

  19. [19]

    https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming28 (2018), e20. https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn

    2018

  20. [20]

    ACM Program

    Finding real bugs in big programs with incorrectness logic.Proc. ACM Program. Lang.6, OOPSLA1 (2022), 1–27. doi:10.1145/3527325 Chunhua Liao, Pei-Hung Lin, Joshua Asplund, Markus Schordan, and Ian Karlin

    doi:10.1145/3527325 2022

  21. [21]

    InProceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis(Denver, Colorado)(SC ’17)

    DataRaceBench: a benchmark suite for systematic evaluation of data race detection tools. InProceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis(Denver, Colorado)(SC ’17). Association for Computing Machinery, New York, NY, USA, Article 11, 14 pages. doi:10.1145/3126908.3126958 Yong Lin, Shange Tang, B...

    work page doi:10.1145/3126908.3126958

  22. [22]

    arXiv:2508.03613 [cs.LG] https://arxiv.org/abs/2508.03613 Gavin Lowe

    Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. arXiv:2508.03613 [cs.LG] https://arxiv.org/abs/2508.03613 Gavin Lowe

    Pith/arXiv arXiv

  23. [23]

    Testing for linearizability.Concurr. Comput. Pract. Exp.29, 4 (2017). doi:10.1002/CPE.3928 Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner

    work page doi:10.1002/cpe.3928 2017

  24. [24]

    263), Karim Ali and Guido Salvaneschi (Eds.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 19:1–19:27. doi:10.4230/ LIPIcs.ECOOP.2023.19 Roland Meyer, Anton Opaterny, Thomas Wies, and Sebastian Wolff

    2023

  25. [25]

    In Computer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proceedings, Part I (Lecture Notes in Computer Science, Vol

    nekton: A Linearizability Proof Checker. In Computer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 13964), Constantin Enea and Akash Lal (Eds.). Springer, 170–183. doi:10.1007/978- 3-031-37706-8_9 Maged M. Michael and Michael L. Scott

    doi:10.1007/978- 2023

  26. [26]

    InProceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing(Philadelphia, Pennsylvania, USA)(PODC ’96)

    Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. InProceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing(Philadelphia, Pennsylvania, USA)(PODC ’96). Association for Computing Machinery, New York, NY, USA, 267–275. doi:10.1145/ 248052.248106 Alexandre Moine, Sam Westrick, and Joseph Tassarotti

    arXiv

  27. [27]

    ACM Program

    All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs.Proc. ACM Program. Lang.10, POPL, Article 26 (Jan. 2026), 29 pages. doi:10.1145/3776668 Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, and Yuanyuan Zhou

    work page doi:10.1145/3776668 2026

  28. [28]

    ACM Program

    Laurel: Unblocking Automated Verification with Large Language Models.Proc. ACM Program. Lang.9, OOPSLA1 (2025), 1519–1545. doi:10.1145/3720499 Peter W. O’Hearn

    doi:10.1145/3720499 2025

  29. [29]

    ACM Program

    Concurrent incorrectness separation logic.Proc. ACM Program. Lang.6, POPL, Article 34 (Jan. 2022), 29 pages. doi:10.1145/3498695 Azalea Raad, Julien Vanegue, Josh Berdine, and Peter O’Hearn

    doi:10.1145/3498695 2022

  30. [30]

    279), Guillermo A

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 279), Guillermo A. Pérez and Jean-François Raskin (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 25:1–25:17. doi:10.4230/LIPIcs.CONCUR.2023.25 Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian...

    doi:10.4230/lipics.concur.2023.25 2023

  31. [31]

    arXiv:2504.21801 [cs.CL] https://arxiv.org/abs/2504.21801 rocq-mcp’s contributors

    DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal 28 Alexandre Moine, Sam Westrick, and Joseph Tassarotti Decomposition. arXiv:2504.21801 [cs.CL] https://arxiv.org/abs/2504.21801 rocq-mcp’s contributors

    Pith/arXiv arXiv

  32. [32]

    https://github.com/LLM4Rocq/rocq-mcp

    rocq-mcp: An MCP Server for the Rocq Prover. https://github.com/LLM4Rocq/rocq-mcp. Accessed: 2026-07-05. Saturn’s contributors

    2026

  33. [33]

    Accessed: 2026-07-06

    https://github.com/ocaml- multicore/saturn. Accessed: 2026-07-06. K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy

    2026

  34. [34]

    2020), 113:1–113:30

    Retrofitting Parallelism onto OCaml.Proceedings of the ACM on Programming Languages 4, ICFP (Aug. 2020), 113:1–113:30. https://doi.org/10.1145/3408995 Daniel Stenberg

    work page doi:10.1145/3408995 2020

  35. [35]

    https://daniel.haxx.se/blog/2026/01/26/the-end-of-the-curl-bug- bounty/

    The end of the curl bug-bounty. https://daniel.haxx.se/blog/2026/01/26/the-end-of-the-curl-bug- bounty/. R. Kent Treiber. 1986.Systems programming: Coping with parallelism. Research Report RJ

    2026

  36. [36]

    InComputer Aided Verification, 22nd International Conference, CA V 2010, Edinburgh, UK, July 15-19,

    Automatically Proving Linearizability. InComputer Aided Verification, 22nd International Conference, CA V 2010, Edinburgh, UK, July 15-19,

    2010

  37. [37]

    Proceedings (Lecture Notes in Computer Science, Vol. 6174). Springer, 450–464. doi:10.1007/978-3-642-14295-6_40 Jeannette M. Wing and Chun Gong

    work page doi:10.1007/978-3-642-14295-6_40

  38. [38]

    Parallel Distributed Comput.17, 1-2 (1993), 164–182

    Testing and Verifying Concurrent Objects.J. Parallel Distributed Comput.17, 1-2 (1993), 164–182. doi:10.1006/JPDC.1993.1015 Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu

    doi:10.1006/jpdc.1993.1015 1993

  39. [39]

    ACM Program

    AutoVerus: Automated Proof Generation for Rust Code.Proc. ACM Program. Lang.9, OOPSLA2 (2025), 3454–3482. doi:10.1145/3763174 He Zhu, Gustavo Petri, and Suresh Jagannathan

    doi:10.1145/3763174 2025

  40. [40]

    InComputer Aided Verification - 27th International Conference, CA V 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science, Vol

    Poling: SMT Aided Linearizability Proofs. InComputer Aided Verification - 27th International Conference, CA V 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 9207). Springer, 3–19. doi:10.1007/978-3-319-21668-3_1 Noam Zilberstein

    work page doi:10.1007/978-3-319-21668-3_1 2015

  41. [41]

    ACM Trans

    Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects. ACM Trans. Program. Lang. Syst.47, 3, Article 14 (Sept. 2025), 71 pages. doi:10.1145/3743131

    doi:10.1145/3743131 2025