{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T21:27:18Z","timestamp":1790112438392,"version":"4.0.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines rules for (i)~forward reasoning using inductive invariants, (ii)~backward reasoning using inductive invariants of a time-reversed system, and (iii)~prophecy steps that add witnesses for existentially quantified properties. We prove each rule sound and give a construction that recovers a single safe inductive invariant from an incremental proof. The construction of the invariant demonstrates the increased complexity of a single inductive invariant compared to the invariant formulas used in an incremental proof, which may have simpler Boolean structures and fewer quantifiers and quantifier alternations. Under natural restrictions on the available invariant formulas, each proof rule strictly increases proof power. That is, each rule allows to prove more safety problems with the same set of formulas. Thus, the incremental approach is able to reduce the search space of invariant formulas needed to prove safety of a given system. A case study on Paxos, several of its variants, and Raft demonstrates that forward-backward steps can remove complex Boolean structure while prophecy eliminates quantifiers and quantifier alternations.<\/jats:p>","DOI":"10.1145\/3808341","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"2354-2378","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4589-2173","authenticated-orcid":false,"given":"Eden","family":"Frenkel","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9380-1939","authenticated-orcid":false,"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Weizmann Institute of Science, Rehovot, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. 1988. The Existence of Refinement Mappings. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science (proceedings of the 3rd annual symposium on logic in computer science ed.). 165\u2013175. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-existence-of-refinement-mappings\/ LICS 1988 Test of Time Award.","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_2"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00571463"},{"key":"e_1_3_2_7_1","volume-title":"Accreditation to supervise research. Institut National Polytechnique de Grenoble - INPG;","author":"Cousot Patrick","year":"1978","unstructured":"Patrick Cousot. 1978. M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique des programmes. Accreditation to supervise research. Institut National Polytechnique de Grenoble - INPG; Universit\u00e9 Joseph-Fourier - Grenoble I. https:\/\/theses.hal.science\/tel-00288657 Universit\u00e9s : Universit\u00e9 scientifique et m\u00e9dicale de Grenoble et Institut national polytechnique de Grenoble."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Ruijie Fang Zachary Kincaid and Thomas Reps. 2025. Software Model Checking via Summary-Guided Search (Extended Version). CoRR abs\/2508.15137 (2025). arXiv:2508.15137 doi:10.48550\/ARXIV.2508.15137","DOI":"10.48550\/ARXIV.2508.15137"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_5"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Eden Frenkel Kenneth McMillan Oded Padon and Sharon Shoham. 2026a. Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy (Artifact). doi:10.5281\/zenodo.19071811","DOI":"10.5281\/zenodo.19071811"},{"key":"e_1_3_2_13_1","doi-asserted-by":"crossref","unstructured":"Eden Frenkel Kenneth L. McMillan Oded Padon and Sharon Shoham. 2026b. Simplifying Safety Proofs with Forward Backward Reasoning and Prophecy. arXiv:2604.15266 [cs.LO] https:\/\/doi.org\/10.48550\/arXiv.2604.15266","DOI":"10.1145\/3808341"},{"key":"e_1_3_2_14_1","first-page":"115","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021,","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021, James Mickens and Renata Teixeira (Eds.). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_3_2_15_1","doi-asserted-by":"crossref","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath T. V. Setty and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles SOSP. 1\u201317.","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0028765"},{"key":"e_1_3_2_17_1","volume-title":"Developing methods for computer programs including a notion of interference.","author":"Jones Cliff B.","year":"1981","unstructured":"Cliff B. Jones. 1981. Developing methods for computer programs including a notion of interference. Ph.D. Dissertation. University of Oxford, UK."},{"key":"e_1_3_2_18_1","first-page":"321","volume-title":"Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983,","author":"Jones Cliff B.","year":"1983","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R.E. A. Mason (Ed.). North-Holland\/IFIP, 321\u2013332."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_18"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"issue":"4","key":"e_1_3_2_23_1","first-page":"18","article-title":"Paxos made simple","volume":"32","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport. 2001. Paxos made simple. ACM SIGACT News 32, 4 (2001), 18\u201325.","journal-title":"ACM SIGACT News"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Leslie Lamport and Stephan Merz. 2022. Prophecy made simple. ACM Transactions on Programming Languages and Systems (TOPLAS) 44 2 (2022) 1\u201327.","DOI":"10.1145\/3492545"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_7"},{"key":"e_1_3_2_26_1","unstructured":"Kenneth L. McMillan. 1992. Symbolic Model Checking: an approach to the state explosion problem. Ph. D. Dissertation. Carnegie Mellon. CMU Tech Rpt. CMU-CS-92-131."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_17"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Kenneth L. McMillan. 2006. Lazy Abstraction with Interpolants. In Computer Aided Verification 18th International Conference CAV 2006 Seattle WA USA August 17-20 2006 Proceedings. 123\u2013136. doi:10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Kenneth L. McMillan. 2018. Eager Abstraction for Symbolic Model Checking. In Computer Aided Verification - 30th International Conference CAV 2018 Held as Part of the Federated Logic Conference FloC 2018 Oxford UK July 14-17 2018 Proceedings Part I (Lecture Notes in Computer Science Vol. 10981) Hana Chockler and Georg Weissenbacher (Eds.). Springer 191\u2013208. doi:10.1007\/978-3-319-96145-3_11","DOI":"10.1007\/978-3-319-96145-3_11"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/101969.101977"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"William Schultz Edward Ashton Heidi Howard and Stavros Tripakis. 2024. Scalable Interpretable Distributed Protocol Verification by Inductive Proof Slicing. CoRR abs\/2404.18048 (2024). arXiv:2404.18048 doi:10.48550\/ARXIV.2404.18048","DOI":"10.48550\/ARXIV.2404.18048"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"William Schultz Ian Dardik and Stavros Tripakis. 2022. Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. In 2022 Formal Methods in Computer-Aided Design (FMCAD). 273\u2013283. doi:10.34727\/2022\/isbn.978-3-85448-053-2_34","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_34"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192414"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-24950-1_15"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_4"},{"key":"e_1_3_2_41_1","first-page":"485","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022,","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022, Marcos K. Aguilera and Hakim Weatherspoon (Eds.). USENIX Association, 485\u2013501. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"e_1_3_2_42_1","first-page":"837","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024,","author":"Zhang Tony Nuda","year":"2024","unstructured":"Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, and Bryan Parno. 2024. Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, Ada Gavrilovska and Douglas B. Terry (Eds.). USENIX Association, 837\u2013853. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/zhang-nuda"},{"key":"e_1_3_2_43_1","first-page":"1","volume-title":"19th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2025, Boston, MA, USA, July 7-9, 2025,","author":"Zhang Tony Nuda","year":"2025","unstructured":"Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, and Bryan Parno. 2025a. Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. In 19th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2025, Boston, MA, USA, July 7-9, 2025, Lidong Zhou and Yuanyuan Zhou (Eds.). USENIX Association, 1\u201317. https:\/\/www.usenix.org\/conference\/osdi25\/presentation\/zhang-tony"},{"key":"e_1_3_2_44_1","unstructured":"Tony Nuda Zhang Keshav Singh Tej Chajed Manos Kapritsos and Bryan Parno. 2025b. Basilisk: Using provenance invariants to automate proofs of undecidable protocols. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25). 1\u201317."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808341","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:39:54Z","timestamp":1790073594000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808341"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":43,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808341"],"URL":"https:\/\/doi.org\/10.1145\/3808341","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}