{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:06Z","timestamp":1784793786458,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Operating a network is a daunting task. Operating one at a global scale, with stringent service objectives and requirements to be available during maintenance and failures, is even more so. At Google, we operate such a network. This paper details our experience applying formal methods to some of the networking protocols that are developed and maintained by in-house engineers. These protocols centrally route network traffic to respond to changes in demand, react to network failures, and allow for maintenance and upgrades.<\/jats:p>\n                  <jats:p>We used formal methods to target a class of bugs stemming from unclear specifications, unintended system interactions, and logical errors at the specification level. We show how we modeled our protocols using an off-the-shelf model checker and a custom harness to scale the model horizontally. We were able to recreate several recent bugs and verify that the fixes implemented were correct. Finally, we present a method called state projection that we used to increase confidence in the coverage of our models, which we added to the TLC model checker for TLA+. We created 7 different TLA+ models and showed that they were effective at recreating bugs and verifying our fixes to those bugs.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_7","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:02Z","timestamp":1784791082000},"page":"136-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking for\u00a0Flexible Network Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-8198","authenticated-orcid":false,"given":"Andrew","family":"Johnson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dennis","family":"Fetterly","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sean","family":"Song","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0315-7316","authenticated-orcid":false,"given":"Jonathan","family":"Zolla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Alberdingk Thijm, T., Beckett, R., Gupta, A., Walker, D.: Modular control plane verification via temporal invariants. Proc. ACM Program. Lang. 7(PLDI), 50\u201375 (2023). ISSN: 2475-1421. https:\/\/doi.org\/10.1145\/3591222","DOI":"10.1145\/3591222"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. SIGPLAN Not. 36(5), 203\u2013213 (2001). ISSN: 0362-1340. https:\/\/doi.org\/10.1145\/381694.378846","DOI":"10.1145\/381694.378846"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_60"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_27"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998, pp. 147\u2013158. Springer, Heidelberg (1998). ISBN: 978-3-540-69339-0","DOI":"10.1007\/BFb0028741"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, Los Angeles, California, pp. 238\u2013252. Association for Computing Machinery (1977). ISBN: 9781450373500. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EA Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382\u2013396. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_25"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/11888116_26","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"Y Fang","year":"2006","unstructured":"Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by invisible invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 356\u2013371. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_26"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. SIGPLAN Not. 37(1), 191\u2013202 (2002). ISSN: 0362-1340. https:\/\/doi.org\/10.1145\/565816.503291","DOI":"10.1145\/565816.503291"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles. SOSP 2015, Monterey, California, pp. 1\u201317. Association for Computing Machinery (2015). ISBN: 9781450338349. https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Hong, C.-Y., et al.: B4 and after: managing hierarchy, partitioning, and asymmetry for availability and scale in Google\u2019s software-defined WAN. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. SIGCOMM 2018, Budapest, Hungary, pp. 74\u201387. Association for Computing Machinery, 2018. ISBN: 9781450355674. https:\/\/doi.org\/10.1145\/3230543.3230545","DOI":"10.1145\/3230543.3230545"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Jain, S., et al.: B4: experience with a globally-deployed software defined wan. SIGCOMM Comput. Commun. Rev. 43(4), 3\u201314 (2013). ISSN: 0146-4833. https:\/\/doi.org\/10.1145\/2534169.2486019","DOI":"10.1145\/2534169.2486019"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-030-81685-8_18","volume-title":"Computer Aided Verification","author":"A Johnson","year":"2021","unstructured":"Johnson, A., Wahl, T.: Delay-bounded scheduling without delay! In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 380\u2013402. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_18"},{"key":"7_CR14","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA (2002). ISBN: 032114306X"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Liu, P., Wahl, T.: CUBA: interprocedural context-unbounded analysis of concurrent programs. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2018, Philadelphia, PA, USA, pp. 105\u2013119. Association for Computing Machinery (2018). ISBN: 9781450356985. https:\/\/doi.org\/10.1145\/3192366.3192419","DOI":"10.1145\/3192366.3192419"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-030-25543-5_22","volume-title":"Computer Aided Verification","author":"P Liu","year":"2019","unstructured":"Liu, P., Wahl, T., Lal, A.: Verifying asynchronous event-driven programs using partial abstract transformers. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 386\u2013404. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_22"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles. SOSP 2019, Huntsville, Ontario, Canada, pp. 370\u2013384. Association for Computing Machinery (2019). ISBN: 9781450368735. https:\/\/doi.org\/10.1145\/3341301.3359651","DOI":"10.1145\/3341301.3359651"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Mace, J., Roelke, R., Fonseca, R.: Pivot tracing: dynamic causal monitoring for distributed systems. In: Proceedings of the 25th Symposium on Operating Systems Principles. SOSP 2015, Monterey, California, pp. 378\u2013393. Association for Computing Machinery (2015). ISBN: 9781450338349. https:\/\/doi.org\/10.1145\/2815400.2815415","DOI":"10.1145\/2815400.2815415"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1), 279\u2013309 (2000). ISSN: 0167-6423. https:\/\/doi.org\/10.1016\/S0167-6423(99)00030-1","DOI":"10.1016\/S0167-6423(99)00030-1"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-96145-3_11","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2018","unstructured":"McMillan, K.L.: Eager abstraction for symbolic model checking. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 191\u2013208. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_11"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Otoni, R., Konnov, I., Kukovec, J., Eugster, P., Sharygina, N.: Symbolic model checking for TLA+ made faster. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 126\u2013144. Springer, Cham (2023). ISBN: 978-3-031-30823-9. https:\/\/doi.org\/10.1007\/978-3-031-30823-9_7","DOI":"10.1007\/978-3-031-30823-9_7"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K. L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. SIGPLAN Not. 51(6), 614\u2013630 (2016). ISSN: 0362-1340. https:\/\/doi.org\/10.1145\/2980983.2908118","DOI":"10.1145\/2980983.2908118"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Sharma, U., Jung, R., Tassarotti, J., Kaashoek, F., Zeldovich, N.: Grove: a separation-logic library for verifying distributed systems. In: Proceedings of the 29th Symposium on Operating Systems Principles, SOSP 2023, Koblenz, Germany, pp. 113\u2013129. Association for Computing Machinery (2023). ISBN: 9798400702297. https:\/\/doi.org\/10.1145\/3600006.3613172","DOI":"10.1145\/3600006.3613172"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Tirmazi, M., et al.: Borg: the next generation. In: Proceedings of the Fifteenth European Conference on Computer Systems. EuroSys 2020, Heraklion, Greece. Association for Computing Machinery (2020). ISBN: 9781450368827. https:\/\/doi.org\/10.1145\/3342195.3387517","DOI":"10.1145\/3342195.3387517"},{"key":"7_CR25","unstructured":"tlaplus. TLA+ Model Checker and Toolbox Source Code (2025). https:\/\/github.com\/tlaplus\/tlaplus. GitHub repository. Accessed 8 Oct 2025"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Verma, A., Pedrosa, L., Korupolu, M., Oppenheimer, D., Tune, E., Wilkes, J.: Large-scale cluster management at Google with Borg. In: Proceedings of the Tenth European Conference on Computer Systems. EuroSys 2015, Bordeaux, France. Association for Computing Machinery (2015). ISBN: 9781450332385. https:\/\/doi.org\/10.1145\/2741948.2741964","DOI":"10.1145\/2741948.2741964"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. SIGPLAN Not. 50(6), 357\u2013368 (2015). ISSN: 0362-1340. https:\/\/doi.org\/10.1145\/2813885.2737958","DOI":"10.1145\/2813885.2737958"},{"key":"7_CR28","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: DistAI: data-driven automated invariant learning for distributed protocols. In: 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2021), pp. 405\u2013421. USENIX Association (2021). ISBN: 978-1-939133-22-9"},{"key":"7_CR29","unstructured":"Yaseen, N., Arzani, B., Beckett, R., Ciraci, S., Liu, V.: Aragog: scalable runtime verification of shardable networked systems. In: Operating systems and implementations (OSDI) (2020). https:\/\/www.microsoft.com\/en-us\/research\/publication\/aragogscalable-runtime-verification-of-shardable-networked-systems\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:04Z","timestamp":1784791084000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The data and artifact for this paper were not made publicly available to retain intellectual property.","order":1,"name":"Ethics","label":"Data Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"Andrew Johnson was employed as a Student Researcher at Google, Inc. while this work was completed. The authors have no competing interests.","order":2,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}