pith. sign in

arxiv: 2606.28066 · v1 · pith:KH46BMSLnew · submitted 2026-06-26 · 💻 cs.PL

Prophecy-Based Automated Verification of Message-Passing Programs

Takashi Nagatomi , Musashi Katsura , Naoki Kobayashi , Yusuke Matsushita , Ken Sakayori This is my paper

Pith reviewed 2026-06-29 01:54 UTC · model grok-4.3

classification 💻 cs.PL
keywords message-passing verificationconstrained Horn clausesprophecy variablesconcurrent programsautomated verificationRust
0
0 comments X

The pith

Message-passing programs reduce to constrained Horn clause satisfiability via prophecy lists of future messages.

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

The paper shows how to verify absence of assertion failures in message-passing concurrent programs by translating them into systems of constrained Horn clauses. Each sender channel becomes a list of values it will send in the future, with added timestamps to record ordering across channels. This representation lets the sender and receiver sides be encoded separately and modularly inside the CHC system. The authors establish that the translation is both sound and complete, so the original program is safe exactly when the generated clauses are satisfiable. A working prototype for Rust-like code confirms the method can be implemented and run on examples.

Core claim

By representing each sender channel as a list of future values augmented with timestamps to capture causal dependencies between channels, the verification problem for message-passing programs is reduced to the satisfiability of a system of constrained Horn clauses, with the reduction proven sound and complete.

What carries the argument

Prophecy representation of each sender channel as a list of future values with timestamps, which modularly encodes sender and receiver threads into CHCs.

If this is right

  • Absence of assertion failures in the program is equivalent to satisfiability of the generated CHCs.
  • Existing CHC solvers can be used directly for the verification task.
  • Sender and receiver threads receive separate modular encodings.
  • The method applies to Rust-like programs as demonstrated by the implemented prototype.

Where Pith is reading between the lines

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

  • The same list-plus-timestamp idea might be adapted to verify programs that use shared memory or other synchronization primitives.
  • Adding support for liveness or termination properties would require extending the CHC encoding beyond safety assertions.
  • The approach could be combined with existing Rust verification tools to handle larger codebases automatically.
  • If the timestamps can be bounded in practice, the encoding might remain efficient even for programs with many channels.

Load-bearing premise

The prophecy list with timestamps for each channel captures every possible behavior of the original program without omitting any real executions or introducing any fake ones.

What would settle it

A concrete message-passing program that triggers an assertion failure yet produces a satisfiable CHC system, or a safe program whose CHC system is unsatisfiable.

Figures

Figures reproduced from arXiv: 2606.28066 by Ken Sakayori, Musashi Katsura, Naoki Kobayashi, Takashi Nagatomi, Yusuke Matsushita.

Figure 8
Figure 8. Figure 8: ◀ B Proof of Soundness and Completeness As briefly explained, the proof of soundness and completeness is given by a mutual construction between (i) a resolution proof of the unsatisfiability and (ii) a reduction sequence of the program leading to an assertion failure. In this section, we first define what a resolution proof is, and then define yet another operational semantics that helps us relate a proof … view at source ↗
Figure 9
Figure 9. Figure 9: Here Merge′ is a function that merges its arguments while preserving the order within each argument list and arranging the result in ascending order of timestamps. Note that we have premises akin to the constraints in the translated CHCs. For example, in EStep-New we require the new prophecies to be sorted. We explain how the content of Cˇ is meant to evolve and what invariants will be maintained. ▶ Defini… view at source ↗
read the original abstract

We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) solving. Inspired by RustHorn's prophecy-based technique, we represent each sender channel by a list of values to be sent over the channel in the future, which enables modular encoding of sender and receiver threads in CHCs. To capture causal dependencies between different channels, we further attach timestamps to messages. We prove that the resulting reduction is sound and complete: a program is free from assertion failures if and only if the corresponding system of CHCs is satisfiable. We have also implemented a prototype verifier for Rust-like programs and experimentally confirmed the effectiveness of the approach.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper proposes a fully automated verification technique for functional correctness (assertion freedom) of message-passing concurrent programs. It reduces the problem to satisfiability of a system of constrained Horn clauses (CHCs) by extending RustHorn-style prophecy variables: each sender channel is encoded as a list of future message values, augmented with timestamps to encode causal dependencies across channels. The central claim is a soundness and completeness theorem establishing that the original program is free of assertion failures if and only if the generated CHC system is satisfiable. The authors also describe a prototype implementation for Rust-like programs and report experimental results.

Significance. If the soundness and completeness result holds, the work would constitute a meaningful advance in automated verification of concurrent programs. It supplies a modular, solver-based encoding that handles message-passing with inter-channel causality via timestamps, and the prototype provides initial evidence of practicality. The explicit reduction to off-the-shelf CHC solvers is a concrete strength that could be reused by other tools.

major comments (1)
  1. [Abstract (central claim)] The soundness and completeness theorem is the load-bearing claim of the paper, yet the provided abstract gives no indication of the proof structure, induction hypotheses, or handling of the timestamp-augmented prophecy lists. Without these details it is impossible to assess whether the encoding of causal dependencies introduces spurious behaviors or loses information, as flagged by the weakest assumption in the reader's report.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We appreciate the referee's feedback on our manuscript. Below we respond to the major comment.

read point-by-point responses

  1. Referee: [Abstract (central claim)] The soundness and completeness theorem is the load-bearing claim of the paper, yet the provided abstract gives no indication of the proof structure, induction hypotheses, or handling of the timestamp-augmented prophecy lists. Without these details it is impossible to assess whether the encoding of causal dependencies introduces spurious behaviors or loses information, as flagged by the weakest assumption in the reader's report.

    Authors: The abstract is designed to provide a concise overview of the proposed method and the main theorem. The proof of soundness and completeness, including the specific induction hypotheses and the role of timestamps in the prophecy lists for preserving causal dependencies, is presented in detail in the main text of the paper. This ensures that the reduction is faithful and does not introduce spurious behaviors or lose information. We can update the abstract to include a short description of the proof approach in a revised version. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper claims a sound and complete reduction from assertion-failure freedom in message-passing programs to CHC satisfiability, using a prophecy encoding of channels as future-value lists augmented with timestamps. The central result is an explicit proof of equivalence between the program property and CHC satisfiability; the encoding is introduced as an extension of external prior work (RustHorn) rather than defined in terms of the target property. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the derivation chain. The result is therefore self-contained against the external CHC solver.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract, no free parameters, axioms, or invented entities are explicitly listed; the approach relies on the unstated assumption that the prophecy encoding preserves semantics.

pith-pipeline@v0.9.1-grok · 5651 in / 1059 out tokens · 21477 ms · 2026-06-29T01:54:43.129580+00:00 · methodology

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

32 extracted references · 19 canonical work pages

  1. [1]

    The existence of refinement mappings

    Mart \' n Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science , 82(2):253--284, 1991

    1991

  2. [2]

    Verifying programs with unreliable channels

    Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993 , pages 160--170. IEEE Computer Society, 1993. https://doi.org/10.1109/LICS.1993.287591 doi:10.1109/LICS.1993.287591

    work page doi:10.1109/lics.1993.287591 1993

  3. [3]

    Principles of Model Checking

    Christel Baier and Joost-Pieter Katoen. Principles of Model Checking . The MIT Press, 2008

    2008

  4. [4]

    Valencia

    Romain Beauxis, Catuscia Palamidessi, and Frank D. Valencia. On the asynchronous nature of the asynchronous pi-calculus. In Pierpaolo Degano, Rocco De Nicola, and Jos \' e Meseguer, editors, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday , Lecture Notes in Computer Science, pages 473--492. Springer, ...

    work page doi:10.1007/978-3-540-68679-8 2008

  5. [5]

    McMillan, and Andrey Rybalchenko

    Nikolaj Bj rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday , volume 9300 of LNCS , pages 24--51. Springer, 2015. https://doi.org/10.1007/978-3-319-23534-9_2 doi:10.1007/978-3-319-23534-9_2

    work page doi:10.1007/978-3-319-23534-9_2 2015

  6. [6]

    Toby Cathcart Burn, C. - H. Luke Ong, and Steven J. Ramsay. Higher-order constrained Horn clauses for verification. Proc. ACM Program. Lang. , 2( POPL ):11:1--11:28, 2018. https://doi.org/10.1145/3158099 doi:10.1145/3158099

    work page doi:10.1145/3158099 2018

  7. [7]

    HoIce : An ICE -based non-linear Horn clause solver

    Adrien Champion, Naoki Kobayashi, and Ryosuke Sato. HoIce : An ICE -based non-linear Horn clause solver. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings , volume 11275 of Lecture Notes in Computer Science , pages 146--156. Springer, 2018. https://doi.or...

    work page doi:10.1007/978-3-030-02768-1 2018

  8. [8]

    Clarke, Orna Grumberg, and Doron A

    Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking . The MIT Press, 1999

    1999

  9. [9]

    Clarke, Thomas A

    Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking . Springer, 2018

    2018

  10. [10]

    Gallagher, Manuel V

    Emanuele De Angelis , Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, and Maurizio Proietti. Analysis and transformation of constrained Horn clauses for program verification. Theory and Practice of Logic Programming , 22(6):974–1042, 2022. https://doi.org/10.1017/S1471068421000211 doi:10.1017/S1471068421000211

    work page doi:10.1017/s1471068421000211 2022

  11. [11]

    Creusot: A foundry for the deductive verification of Rust programs

    Xavier Denis, Jacques-Henri Jourdan, and Claude March \'e . Creusot: A foundry for the deductive verification of Rust programs. In International Conference on Formal Engineering Methods , pages 90--105. Springer, 2022

    2022

  12. [12]

    Freund, and Shaz Qadeer

    Cormac Flanagan, Stephen N. Freund, and Shaz Qadeer. Thread-modular verification for shared-memory programs. In Daniel Le M \' e tayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 200...

    work page doi:10.1007/3-540-45927-8 2002

  13. [13]

    VerusBelt : A semantic foundation for Verus 's proof-oriented extensions to the Rust type system

    Travis Hance, Laila Elbeheiry, Yusuke Matsushita, and Derek Dreyer. VerusBelt : A semantic foundation for Verus 's proof-oriented extensions to the Rust type system. Proc. ACM Program. Lang. , 10(PLDI), June 2026. https://doi.org/10.1145/3808325 doi:10.1145/3808325

    work page doi:10.1145/3808325 2026

  14. [14]

    Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer

    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In Warren A. Hunt Jr. and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings , Lecture Notes in Computer Science, pages 262--274. Springer, 2003. https://doi.or...

    work page doi:10.1007/978-3-540-45069-6 2003

  15. [15]

    The ELDARICA Horn solver

    Hossein Hojjat and Philipp R \"u mmer. The ELDARICA Horn solver. In 2018 Formal Methods in Computer Aided Design (FMCAD) , pages 1--7. IEEE, 2018

    2018

  16. [16]

    Foundations of session types and behavioural contracts

    Hans H \"u ttel, Ivan Lanese, Vasco T Vasconcelos, Lu \' s Caires, Marco Carbone, Pierre-Malo Deni \'e lou, Dimitris Mostrous, Luca Padovani, Ant \'o nio Ravara, Emilio Tuosto, et al. Foundations of session types and behavioural contracts. ACM Computing Surveys (CSUR) , 49(1):1--36, 2016

    2016

  17. [17]

    The future is ours: prophecy variables in separation logic

    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. Proceedings of the ACM on Programming Languages , 4(POPL):1--32, 2019

    2019

  18. [18]

    Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, Indi...

    work page doi:10.1145/2676726.2676980 2015

  19. [19]

    Automated catamorphism synthesis for solving constrained Horn clauses over algebraic data types

    Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. Automated catamorphism synthesis for solving constrained Horn clauses over algebraic data types. In International Static Analysis Symposium , pages 305--327. Springer, 2025

    2025

  20. [20]

    Type systems for concurrent programs

    Naoki Kobayashi. Type systems for concurrent programs. In Formal Methods at the Crossroads. From Panacea to Foundational Support: 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002. Revised Papers , pages 439--453. Springer, 2003

    2002

  21. [21]

    Temporal verification of programs via first-order fixpoint logic

    Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. Temporal verification of programs via first-order fixpoint logic. In Bor - Yuh Evan Chang, editor, Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings , volume 11822 of Lecture Notes in Computer Science , pages 413--436. Springer,...

    work page doi:10.1007/978-3-030-32304-2 2019

  22. [22]

    HFL(Z) validity checking for automated program verification

    Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada. HFL(Z) validity checking for automated program verification. Proc. ACM Program. Lang. , 7( POPL ):154--184, 2023. https://doi.org/10.1145/3571199 doi:10.1145/3571199

    work page doi:10.1145/3571199 2023

  23. [23]

    Higher-order program verification via HFL model checking

    Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. Higher-order program verification via HFL model checking. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 201...

    work page doi:10.1007/978-3-319-89884-1 2018

  24. [24]

    SMT -based model checking for recursive programs

    Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. SMT -based model checking for recursive programs. Formal Methods Syst. Des. , 48(3):175--205, 2016. URL: https://doi.org/10.1007/s10703-016-0249-4

    work page doi:10.1007/s10703-016-0249-4 2016

  25. [25]

    Verus: Verifying Rust programs using linear ghost types

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proc. ACM Program. Lang. , 7( OOPSLA1 ):286--315, 2023. https://doi.org/10.1145/3586037 doi:10.1145/3586037

    work page doi:10.1145/3586037 2023

  26. [26]

    Precise thread-modular verification

    Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Precise thread-modular verification. In Hanne Riis Nielson and Gilberto Fil \'e , editors, Static Analysis , pages 218--232, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg

    2007

  27. [27]

    RustHornBelt : A semantic foundation for functional verification of Rust programs with unsafe code

    Yusuke Matsushita, Xavier Denis, Jacques - Henri Jourdan, and Derek Dreyer. RustHornBelt : A semantic foundation for functional verification of Rust programs with unsafe code. In Ranjit Jhala and Isil Dillig, editors, PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 20...

    work page doi:10.1145/3519939.3523704 2022

  28. [28]

    Nola: Later-free ghost state for verifying termination in Iris

    Yusuke Matsushita and Takeshi Tsukada. Nola: Later-free ghost state for verifying termination in Iris . Proc. ACM Program. Lang. , 9( PLDI ):98--124, 2025. https://doi.org/10.1145/3729250 doi:10.1145/3729250

    work page doi:10.1145/3729250 2025

  29. [29]

    RustHorn : CHC -based verification for Rust programs

    Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. RustHorn : CHC -based verification for Rust programs. ACM Transactions on Programming Languages and Systems (TOPLAS) , 43(4):1--54, 2021

    2021

  30. [30]

    Thrust: A prophecy-based refinement type system for Rust

    Hiromi Ogawa, Taro Sekiyama, and Hiroshi Unno. Thrust: A prophecy-based refinement type system for Rust . Proc. ACM Program. Lang. , 9( PLDI ):2056--2080, 2025. https://doi.org/10.1145/3729333 doi:10.1145/3729333

    work page doi:10.1145/3729333 2056

  31. [31]

    Practical refinement session type inference

    Toby Ueno and Ankush Das. Practical refinement session type inference. In Robbert Krebbers, editor, Programming Languages and Systems , pages 298--330, Cham, 2026. Springer Nature Switzerland

    2026

  32. [32]

    Modular primal-dual fixpoint logic solving for temporal verification

    Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang. , 7( POPL ):2111--2140, 2023. https://doi.org/10.1145/3571265 doi:10.1145/3571265

    work page doi:10.1145/3571265 2023