Pith. sign in

REVIEW 2 major objections 5 minor 29 references

A Systematic Literature Review on a Decade of Industrial TLA+ Practice

T0 review · 2 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read A systematic review of a decade of industry reports finds TLA+ adoption surging since 2015, led by cloud systems.

desk verdict A useful, transparent SLR on industrial TLA+ that overreaches in its RQ1 trend claim; the qualitative synthesis is the real contribution. read the letter →

arxiv 2411.13722 v1 pith:XM2PW7VP submitted 2024-11-20 cs.SE

Roman Bögli , Leandro Lerena , Christos Tsigkanos , Timo Kehrer This is my paper · ORCID
classification cs.SE
keywords TLA+PlusCalformalmethodssystematicliteraturereviewindustrialadoptionmodelcheckingcloudcomputingsoftwareengineering
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper sets out to establish, through a systematic review of the past decade, that TLA+—a formal specification language for describing and model-checking system behavior—has moved into real industrial use, and that this use is growing and concentrated in specific settings. It argues that industry reports since 2015 show adoption surging, particularly for cloud systems, where TLA+ is used mostly during early design and debugging rather than during implementation. The review claims these reports confirm TLA+'s promised benefits: finding subtle bugs such as deadlocks and race conditions and improving system understanding, while also surfacing two persistent obstacles, a steep learning curve and difficulty choosing the right abstraction level. A sympathetic reader would care because the findings give practitioners a curated evidence base for deciding whether to adopt TLA+ and give researchers a map of where tooling and training should improve.

What carries the argument

The review mechanism is a three-stage systematic literature review: an optimistic Google Scholar search with a keyword string combining TLA+ and PlusCal with practice and industry terms, followed by a reduction pipeline of deduplication (290 to 261 papers), rejection (261 to 37), and an affinity filter scoring each paper on reasons for using formal methods, modeling assumptions, the model-implementation link, and practical drawbacks (37 to 16 high-affinity papers). A linear regression on the 261 deduplicated papers supplies the trend answer for RQ1, while the 16 high-affinity papers provide the qualitative evidence for application settings, benefits, and challenges.

What would settle it

If a re-run of the same Google Scholar search string over the same period produced a flat or declining deduplicated count, or if the linear regression on the 16 high-affinity papers alone (rather than the 261 deduplicated papers) had $p \ge 0.05$, the paper's 'significant upward trend' and 'surge since 2015' claims would not be supported. The paper itself reports the regression only for the 261-paper set and notes that set may include irrelevant or nonsensical papers.

Watch

Extended reading notes

Core claim

The paper claims that TLA+, a temporal-logic specification language with the PlusCal front-end, has moved from a niche academic tool to a growing industrial practice over 2013-2023. Analyzing 290 initially found publications and, after filtering, 16 high-affinity industry reports, it concludes that TLA+ usage has surged since 2015, is most common in the cloud industry (63% of the included papers), and is applied mainly during early design and debugging. The reports consistently credit TLA+ with finding subtle bugs and improving system understanding, while naming a steep learning curve and abstraction-level choice as the main barriers. The review frames the Amazon Web Services report [10] as a catalyst because 44% of the included papers cite it as motivation. The overall upward trend is quantified by a linear regression on the 261 deduplicated papers with slope $S = 3.67$ and $p < 0.001$.

Load-bearing premise

The review's trend and surge conclusions rest on the assumption that the 261 deduplicated Google Scholar matches—which the authors concede may include irrelevant or nonsensical papers—accurately track industrial TLA+ activity rather than academic output or search-engine noise.

Editorial extensions

If this is right

  • Industrial TLA+ use is concentrated in cloud computing, with more than 60% of the high-affinity papers in that domain.
  • TLA+ is mostly used during early design (81% of label occurrences), then debugging (44%), and least during implementation (38%).
  • Practitioners report that TLA+ finds subtle bugs such as deadlocks, race conditions, and stack overflow errors, and that it improves overall system understanding.
  • Adoption is hindered by a steep learning curve and by difficulty choosing the right abstraction level; PlusCal is seen as easing the learning curve.
  • The significant upward trend in TLA+ publications is likely to continue because success stories such as the Amazon Web Services report are cited as motivators by later adopters.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: if the observed cross-company contagion holds, formal-specification skills could become a visible differentiator in cloud-infrastructure hiring within a few years.
  • Beyond the paper: the 63% cloud concentration suggests that the next high-impact TLA+ targets are cloud control planes and consensus protocols, where the state space is bounded enough for exhaustive model checking.
  • Beyond the paper: the Google-Scholar-only corpus cannot see proprietary or defunct industrial work, so the true adoption curve may be steeper or shallower than reported; interviews, surveys, or a second search engine would test which.
  • Beyond the paper: applying the same affinity filter to other formal methods such as Alloy, B, or VDM would show whether the post-2015 surge is TLA+-specific or part of a broader formal-methods revival.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. The paper is a systematic literature review (SLR) of industrial TLA+ practice from 2013 to 2023. It defines four research questions on trend, characterization, benefits, and challenges of TLA+ in industry. The authors use a Google Scholar search with a compound query (Listing 1), reduce 290 initial hits to 16 'high-affinity' papers via deduplication, exclusion, and an affinity filter, and then analyze those 16 papers. The paper claims a statistically significant upward trend in TLA+ publications (based on 261 deduplicated hits, S=3.67, p<0.001), characterizes industrial use as predominantly cloud-oriented and concentrated in early design/debugging, and reports that TLA+ delivers bug-finding and design-understanding benefits while facing steep learning curve and abstraction challenges. The filtered dataset is published on Zenodo.

Significance. If the trend claim were supported, the paper would be a valuable empirical contribution on formal-methods adoption in industry. The paper's strengths include a transparent and reproducible search string, a published dataset, independent dual coding with author adjudication, and a clear qualitative synthesis of 16 industrial case studies. The RQ2-RQ4 findings—cloud dominance, early-design usage, reported bug-finding benefits, and challenge themes—are useful for both practitioners and researchers. The main significance hinges on the RQ1 trend estimate, which currently conflates publication volume with industrial usage and lacks the data needed to support the 'surge' conclusion.

major comments (2)
  1. [Section 3.1 and Section 5] The central RQ1 answer—'There is a significant upward trend in TLA+ papers in general, which is likely to continue due to success stories'—and the concluding 'surge since 2015' are based on a linear regression of the 261 deduplicated Google Scholar hits, not on the 16 high-affinity papers that actually concern industrial use. The search string in Listing 1 is a broad compound query over general terms ('application', 'practice', 'insight', 'usage') and industry names, so the 261-paper series is a measure of publication volume matching those terms, not of industrial TLA+ adoption. The authors themselves state in Section 4 that this set 'may include irrelevant or nonsensical papers, which potentially skews our trend analysis.' No baseline comparison (e.g., TLA+ papers without industry terms, or another formal method) is provided to allow the upward slope to be attributed to industry practice. This is a load-bearing flaw in the paper's main contribution.
  2. [Section 3.1 and Figure 1] The regression reporting is incomplete and the extrapolation is unsupported. The paper reports only the slope (S=3.67) and p-value; it gives no confidence intervals, R², model diagnostics, or sensitivity analysis with respect to the query wording or time range. More importantly, no trend test is run on the 16 high-affinity papers, and those counts are too sparse and variable (e.g., the 2020 peak and missing years in the accepted subset in Figure 1) to justify the conclusion 'TLA+ usage has surged since 2015.' The statement that the trend 'is likely to continue' is a prediction unsupported by either the regression or the qualitative data. At minimum, the RQ1 answer should be restricted to 'publications matching the search query increased,' with the industrial-adoption claim presented as a qualitative observation from the 16 case studies.
minor comments (5)
  1. [Figure 1] The stacked bar chart is difficult to read; please add a table with the exact per-year counts for each category (optimistic, deduplicated, rejected, low-affinity, high-affinity).
  2. [Section 4] The sentence 'which potentially skews our trend analysis and leading to misleading conclusions' should be rephrased, e.g., 'which could skew our trend analysis and lead to misleading conclusions.'
  3. [Section 3.1] The phrase 'This insight of a growing overall trend' should be 'This observation of a growing overall trend.'
  4. [Section 2.2] The exclusion criterion 'no access to paper over university network' may introduce accessibility bias; please discuss this in the threats to validity section.
  5. [Section 2.2] No inter-rater reliability measure (e.g., Cohen's kappa) is reported for the screening and affinity-scoring phases; please add such a measure or justify its absence.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the SLR findings are aggregations of the collected corpus, not derivations from their own conclusions.

full rationale

This paper is a systematic literature review, and its conclusions are summaries and counts of the 16 high-affinity papers plus a linear regression over the 261 deduplicated Google Scholar results. No equation is fitted and then reported as an independent prediction; no parameter is calibrated on one subset to explain the same subset under a new name; and no load-bearing self-citation or imported uniqueness theorem is used. The RQ1 trend is computed directly from the paper's own search corpus, and the authors explicitly acknowledge its limits: in Section 3.1 they note that 'the overall growth trend does not directly address TLA+ usage in industrial settings,' and in Section 4 they warn that the 261-paper set 'may include irrelevant or nonsensical papers, which potentially skews our trend analysis.' The conclusion that 'TLA+ usage has surged since 2015' is broader than the regression strictly supports, but this is a validity and inference concern about corpus coverage and generalization, not circularity in which the conclusion is identical to the input by construction. The affinity filter and card-sorting choices are disclosed methodological selections rather than hidden assumptions that smuggle the results in. The paper is self-contained against its stated evidence base, so the most honest finding is no circularity.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

This SLR has no free numeric model parameters or invented entities. Its conclusions rest on the chosen search corpus, the affinity threshold, and manual coding assumptions, all of which the authors acknowledge as threats to validity.

free parameters (1)
  • Affinity filter score threshold = 3.5 / 4 points
    Hand-chosen cutoff in Section 2.2; determines which 16 of 37 papers are included, and therefore shapes all RQ2-RQ4 conclusions.
assumptions (4)
  • domain assumption Google Scholar indexes all relevant industrial TLA+ reports, including grey literature.
    Section 2.1 states reliance exclusively on Google Scholar; Section 4 acknowledges this may miss IP-protected or non-indexed work.
  • domain assumption The optimistically collected 261 deduplicated papers are a meaningful basis for inferring an industrial TLA+ trend.
    Section 3.1 uses the 261 set for the linear regression, though it may contain irrelevant papers; this is acknowledged as a validity threat.
  • domain assumption The four affinity questions measure a paper's suitability to answer the research questions.
    Section 2.2 defines the affinity filter; there is no independent validation of this construct beyond author judgment.
  • domain assumption The industry categories from card sorting are independent and meaningful.
    Section 3.2 describes open card sorting; the mapping of 16 papers to cloud, railway, control, blockchain, transportation is subjective.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Systematic Literature Review on a Decade of Industrial TLA+ Practice." pith.science (2026). https://pith.science/paper/XM2PW7VP

@misc{pith2026241113722,
  author       = {Pith},
  title        = {Pith review of: A Systematic Literature Review on a Decade of Industrial TLA+ Practice},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XM2PW7VP}},
  note         = {Machine review of arXiv:2411.13722}
}
read the original abstract

TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in practice remains scarce. Industry reports suggest that software engineers could benefit from insights, innovations, and solutions to the practical challenges of TLA+. This paper explores this development by conducting a systematic literature review of TLA+'s industrial usage over the past decade. We analyze the trend in industrial application, characterize its use, examine whether its promised benefits resonate with practitioners, and identify challenges that may hinder further adoption.

Figures

Figures reproduced from arXiv: 2411.13722 by the authors.

Figure 1
Figure 1. Paper qualifying process, resulting in 16 relevant ones for this SLR. in this SLR4 . To differentiate these from other references in this paper, we have numbered them accordingly (1-16) and subdivided the bibliography into two sections. 3 Results The 16 included papers could be linked to some well-known companies or prod￾ucts. This includes Abaco Autoscaler [11], Alibaba Group (Alibaba PolarDB) [4], Amazon Web Servi… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 18 canonical work pages

  1. [1]

    A Tendermint Light Client

    Braithwaite, S., Buchman, E., Khoffi, I., Konnov, I., Milosevic, Z., Ruetschi, R., Widder, J.: A Tendermint Light Client (Oct 2020). https://doi.org/10.48550/arX iv.2010.07031

    work page Pith review arXiv doi:10.48550/arxiv.2010.07031 2020

  2. [2]

    Pro- ceedings of the VLDB Endowment13(9), 1346–1358 (May 2020)

    Davis, A.J.J., Hirschhorn, M., Schvimer, J.: eXtreme Modelling in Practice. Pro- ceedings of the VLDB Endowment13(9), 1346–1358 (May 2020). https://doi.or g/10.14778/3397230.3397233

    arXiv 2020

  3. [3]

    In: Huisman, M., Păsăreanu, C., Zhan, N

    Gao, S., Zhan, B., Liu, D., Sun, X., Zhi, Y., Jansen, D.N., Zhang, L.: Formal Verification of Consensus in the Taurus Distributed Database. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) Formal Methods. pp. 741–751. Springer Interna- tional Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_42

    work page doi:10.1007/978-3-030-90870-6_42 2021

  4. [4]

    In: 2022 41st International Symposium on Reliable Distributed Systems (SRDS)

    Gu, X., Cao, W., Zhu, Y., Song, X., Huang, Y., Ma, X.: Compositional Model Checking of Consensus Protocols via Interaction-Preserving Abstraction. In: 2022 41st International Symposium on Reliable Distributed Systems (SRDS). pp. 82–93 (Sep 2022). https://doi.org/10.1109/SRDS55811.2022.00018

    work page arXiv 2022

  5. [5]

    Hackett, F., Rowe, J., Kuppe, M.A.: Going Beyond an Incident Report with TLA+ (Jul 2023), https://www.usenix.org/sites/default/files/login_-_going_beyond _an_incident_report_with_tla_.pdf

    work page 2023

  6. [6]

    In: 2023 IEEE/ACM 45th International Conference on Soft- ware Engineering: Software Engineering in Practice (ICSE-SEIP)

    Hackett, F., Rowe, J., Kuppe, M.A.: Understanding Inconsistency in Azure Cos- mos DB with TLA+. In: 2023 IEEE/ACM 45th International Conference on Soft- ware Engineering: Software Engineering in Practice (ICSE-SEIP). pp. 1–12. IEEE (2023). https://doi.org/10.1109/ICSE-SEIP58684.2023.00006

    arXiv 2023

  7. [7]

    In: Proceedings of the 5th ACM Computer Science in Cars Symposium

    Jakobs, C., Werner, M., Schmidt, K., Hansch, G.: Following the White Rabbit: Integrity Verification Based on Risk Analysis Results. In: Proceedings of the 5th ACM Computer Science in Cars Symposium. pp. 1–9. CSCS ’21, Association for Computing Machinery, New York, NY, USA (Nov 2021). https://doi.org/10.114 5/3488904.3493377

    arXiv 2021

  8. [8]

    In: Artho, C., Ölveczky, P.C

    Methni, A., Lemerre, M., Ben Hedia, B., Haddad, S., Barkaoui, K.: Specifying and Verifying Concurrent C Programs with TLA+. In: Artho, C., Ölveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. pp. 206–222. Springer International Publishing, Cham (2015). https://doi.org/10.1007/978-3-319-17581-2_14

    work page doi:10.1007/978-3-319-17581-2_14 2015

Show all 29 references
  1. [9]

    In: Ait Ameur, Y., Schewe, K.D

    Newcombe, C.: Why Amazon Chose TLA+. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. pp. 25–39. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_3

    2014 doi

  2. [10]

    Communications of the ACM 58(4), 66–73 (Mar 2015)

    Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Communications of the ACM 58(4), 66–73 (Mar 2015). https://doi.org/10.1145/2699417

    2015 doi

  3. [11]

    In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N

    Padhy, S., Stubbs, J.: Designing and Proving Properties of the Abaco Autoscaler Using TLA+. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification. pp. 86–103. Springer International Publishing, Cham (2022). https: //doi.org/10.1007/978-3-030-95561-8_6

    2022 doi

  4. [12]

    In: 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)

    Resch, S., Paulitsch, M.: Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware. In: 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). pp. 146–152 (Oct 2017). https: //doi.org/10.1109/ISSREW.2017.43

    2017 doi

  5. [13]

    https: //doi.org/10.48550/arXiv.1911.11286 10 R

    Roohitavaf, M., Ren, K., Zhang, G., Ben-romdhane, S.: LogPlayer: Fault-tolerant Exactly-once Delivery using gRPC Asynchronous Streaming (Nov 2019). https: //doi.org/10.48550/arXiv.1911.11286 10 R. Bögli et al

    2019 doi arXiv

  6. [14]

    In: Staggs, J., Shenoi, S

    Sabraoui, M., Hieb, J., Lauf, A., Graham, J.: Modeling and Machine-Checking Bump-in-the-Wire Security for Industrial Control Systems. In: Staggs, J., Shenoi, S. (eds.) Critical Infrastructure Protection XIII. pp. 271–288. Springer Interna- tional Publishing, Cham (2019). https...

    2019 doi

  7. [15]

    In: 2020 IEEE 29th In- ternational Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE)

    Salierno, G., Morvillo, S., Leonardi, L., Cabri, G.: Specification and verification of railway safety-critical systems using TLA+: A Case Study. In: 2020 IEEE 29th In- ternational Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). pp. 2...

    2020

  8. [16]

    https://doi.org/10.48550/arXiv.2 102.11960 References (Other)

    Schultz, W., Zhou, S., Dardik, I., Tripakis, S.: Design and Analysis of a Logless Dynamic Reconfiguration Protocol (Nov 2021). https://doi.org/10.48550/arXiv.2 102.11960 References (Other)

    2021 doi

  9. [17]

    ACM Computing Surveys 51(5), 105:1–105:38 (Nov 2018)

    Buyya,R.,Srirama,S.N.,Casale,G.,Calheiros,R.,Simmhan,Y.,Varghese,B.,Ge- lenbe, E., Javadi, B., Vaquero, L.M., Netto, M.A.S., Toosi, A.N., Rodriguez, M.A., Llorente, I.M., Vimercati, S.D.C.D., Samarati, P., Milojicic, D., Varela, C., Bah- soon, R., Assuncao, M.D.D., Rana, O., Z...

    2018

  10. [18]

    MethodsX9, 101895 (Jan 2022)

    Carrera-Rivera, A., Ochoa, W., Larrinaga, F., Lasa, G.: How-to conduct a system- atic literature review: A quick guide for computer science research. MethodsX9, 101895 (Jan 2022). https://doi.org/10.1016/j.mex.2022.101895

    2022

  11. [19]

    In: Meyer, B., Nordio, M

    Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model Checking and the State Explosion Problem. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification: LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, pp. 1–30. Sp...

    2012 doi

  12. [20]

    Technological Forecasting and Social Change108, 28–41 (Jul 2016)

    Dedehayir, O., Steinert, M.: The hype cycle model: A review and future directions. Technological Forecasting and Social Change108, 28–41 (Jul 2016). https://doi. org/10.1016/j.techfore.2016.04.005

    2016 doi

  13. [21]

    Kitchenham, B.A., Charters, S.: Guidelines for performing systematic literature reviews in software engineering. Tech. Rep. EBSE 2007-001, Keele University and Durham University Joint Report (07 2007), https://www.elsevier.com/__data/ promis_misc/525444systematicreviewsguide.pdf

    2007

  14. [22]

    Addison-Wesley (Jun 2002), https://www.microsoft.co m/en-us/research/uploads/prod/2018/05/book-02-08-08.pdf

    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (Jun 2002), https://www.microsoft.co m/en-us/research/uploads/prod/2018/05/book-02-08-08.pdf

    2002

  15. [23]

    In: Leucker, M., Morgan, C

    Lamport, L.: The PlusCal Algorithm Language. In: Leucker, M., Morgan, C. (eds.) Theoretical Aspects of Computing - ICTAC 2009. pp. 36–60. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03466-4_2

    2009 doi

  16. [24]

    Information and Software Technology 64, 1–18 (Aug 2015)

    Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: An update. Information and Software Technology 64, 1–18 (Aug 2015). https://doi.org/10.1016/j.infsof.2015.03.007

    2015 doi

  17. [25]

    In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp. 46–57 (Oct 1977). https: //doi.org/10.1109/SFCS.1977.32 SLR on Industrial TLA+Usage 11

    1977 doi

  18. [26]

    https://doi.org/10.48550/arXiv.2010.16345

    Reid, A., Church, L., Flur, S., de Haas, S., Johnson, M., Laurie, B.: Towards making formal methods normal: meeting developers where they are (Oct 2020). https://doi.org/10.48550/arXiv.2010.16345

    2020 doi arXiv

  19. [27]

    Social science, Free Press, New York Lon- don Toronto Sydney, 5 edn

    Rogers, E.M.: Diffusion of Innovations. Social science, Free Press, New York Lon- don Toronto Sydney, 5 edn. (2003), ISBN: 978-0-7432-2209-9

    2003

  20. [28]

    IEEE Access8, 36226–36243 (2020)

    Yasin, A., Fatima, R., Wen, L., Afzal, W., Azhar, M., Torkar, R.: On Using Grey Literature and Google Scholar in Systematic Literature Reviews in Software En- gineering. IEEE Access8, 36226–36243 (2020). https://doi.org/10.1109/ACCESS .2020.2971712

    2020

  21. [29]

    In: Menzies, T., Williams, L., Zimmermann, T

    Zimmermann, T.: Card-sorting: From text to themes. In: Menzies, T., Williams, L., Zimmermann, T. (eds.) Perspectives on Data Science for Software Engineering, pp. 137–141. Morgan Kaufmann, Boston (Jan 2016). https://doi.org/10.1016/B9 78-0-12-804206-9.00027-1

    2016 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.