{"id":935385,"date":"2023-04-24T09:00:00","date_gmt":"2023-04-24T16:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=935385"},"modified":"2023-05-05T10:35:43","modified_gmt":"2023-05-05T17:35:43","slug":"tla-foundation-aims-to-bring-math-based-software-modeling-to-the-mainstream","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/tla-foundation-aims-to-bring-math-based-software-modeling-to-the-mainstream\/","title":{"rendered":"TLA+ Foundation aims to bring math-based software modeling to the mainstream"},"content":{"rendered":"\n<figure class=\"wp-block-image size-full\"><img loading=\"lazy\" decoding=\"async\" width=\"1400\" height=\"788\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1.jpg\" alt=\"Leslie Lamport headshot in front of blurred code\" class=\"wp-image-936024\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1.jpg 1400w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-300x169.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1024x576.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-768x432.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1066x600.jpg 1066w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-655x368.jpg 655w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-343x193.jpg 343w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-240x135.jpg 240w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-640x360.jpg 640w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-960x540.jpg 960w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1280x720.jpg 1280w\" sizes=\"auto, (max-width: 1400px) 100vw, 1400px\" \/><\/figure>\n\n\n\n<p>TLA+ is a high level, open-source, math-based language for modeling computer programs and systems\u2013especially concurrent and distributed ones.&nbsp;It comes with tools to help eliminate fundamental design errors, which are hard to find and expensive to fix once they have been embedded in code or hardware.&nbsp;<\/p>\n\n\n\n<p>The <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-temporal-logic-of-actions\/\" target=\"_blank\" rel=\"noreferrer noopener\">TLA language<\/a> was first published in 1993 by the pioneering computer scientist <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/lamport\/\" target=\"_blank\" rel=\"noreferrer noopener\">Leslie Lamport<\/a>, now a distinguished scientist with Microsoft Research. After years of Lamport\u2019s stewardship and Microsoft\u2019s support, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/lamport.azurewebsites.net\/tla\/tla.html\" target=\"_blank\" rel=\"noopener noreferrer\">TLA+<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> has found a new home. The TLA+ Foundation is launching this month as part of the Linux Foundation, with Microsoft, Amazon Web Services (AWS), and Oracle serving as founding members to help further refine the tools and spur commercial usage and additional research.&nbsp;<\/p>\n\n\n\n<p>\u201cThe foundation will help spread that work among more hands,\u201d said Lamport.&nbsp;<\/p>\n\n\n\n<p>TLA+ is just one piece of Lamport\u2019s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/lamport.azurewebsites.net\/pubs\/pubs.html\" target=\"_blank\" rel=\"noopener noreferrer\">impressive portfolio<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>. He invented the document preparation system <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/www.latex-project.org\/\" target=\"_blank\" rel=\"noopener noreferrer\">LaTeX<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and won the 2013 <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/amturing.acm.org\/award_winners\/lamport_1205376.cfm\" target=\"_blank\" rel=\"noopener noreferrer\">Turing Award<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> for his work to clarify distributed systems, in which several autonomous computers communicate with each other by passing messages.\u00a0<\/p>\n\n\n\n<div style=\"height:15px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n\t<div class=\"border-bottom border-top border-gray-300 mt-5 mb-5 msr-promo text-center text-md-left alignwide\" data-bi-aN=\"promo\" data-bi-id=\"1141385\">\n\t\t\n\n\t\n\t<div class=\"row pt-3 pb-4 align-items-center\">\n\t\t\t\t\t\t<div class=\"msr-promo__media col-12 col-md-5\">\n\t\t\t\t<a class=\"bg-gray-300 display-block\" href=\"https:\/\/ai.azure.com\/labs\" aria-label=\"Azure AI Foundry Labs\" data-bi-cN=\"Azure AI Foundry Labs\" target=\"_blank\">\n\t\t\t\t\t<img decoding=\"async\" class=\"w-100 display-block\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/06\/Azure-AI-Foundry_1600x900.jpg\" \/>\n\t\t\t\t<\/a>\n\t\t\t<\/div>\n\t\t\t\n\t\t\t<div class=\"msr-promo__content p-3 px-5 col-12 col-md\">\n\n\t\t\t\t\t\t\t\t\t<h2 class=\"h4\">Azure AI Foundry Labs<\/h2>\n\t\t\t\t\n\t\t\t\t\t\t\t\t<p id=\"azure-ai-foundry-labs\" class=\"large\">Get a glimpse of potential future directions for AI, with these experimental technologies from Microsoft Research.<\/p>\n\t\t\t\t\n\t\t\t\t\t\t\t\t<div class=\"wp-block-buttons justify-content-center justify-content-md-start\">\n\t\t\t\t\t<div class=\"wp-block-button\">\n\t\t\t\t\t\t<a href=\"https:\/\/ai.azure.com\/labs\" aria-describedby=\"azure-ai-foundry-labs\" class=\"btn btn-brand glyph-append glyph-append-chevron-right\" data-bi-cN=\"Azure AI Foundry Labs\" target=\"_blank\">\n\t\t\t\t\t\t\tAzure AI Foundry\t\t\t\t\t\t<\/a>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t<\/div><!--\/.msr-promo__content-->\n\t<\/div><!--\/.msr-promo__inner-wrap-->\n\t<\/div><!--\/.msr-promo-->\n\t\n\n\n<p>Along the way he developed an idea to help programmers build systems more effectively by using algorithmic models to specify how the code should work. It\u2019s the same idea as creating blueprints to guide the construction of a bridge. TLA+ (for Temporal Logic of Actions) comes with a model checker that will check whether satisfying a program\u2019s specification implies that the code will do what it should.<\/p>\n\n\n\n<p>\u201cWhen programmers write systems, they should start by defining what they are supposed to do and check that their work will do it. That\u2019s a better way than just sitting down to write the code, based on some vague outline,\u201d Lamport said.&nbsp;<\/p>\n\n\n\n<p>For simple tasks, a trial-and-error approach may be fine. But for more complicated projects, or those where mistakes are unacceptable, a systematic approach makes more sense.<\/p>\n\n\n\n<p>The challenge with writing large programs isn\u2019t necessarily their size, it\u2019s their complexity. They are often distributed across multiple systems and involve multiple processes that need to interact. The number of possible executions becomes astronomical. To reason about and check such a system, it helps to have a mathematical way to think about it ahead of time. Yet&nbsp;engineers often balk at the idea.&nbsp;<\/p>\n\n\n\n<p>\u201cThe difficulty that engineers have is more a fear of math than the math itself. The math, as math goes, is very basic,\u201d Lamport said, though it\u2019s worth noting he holds a PhD in mathematics. \u201cI find that engineers, after using TLA+, understand the benefit.\u201d<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"475\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1-1024x475.jpg\" alt=\"Leslie Lamport giving a talk on stage\" class=\"wp-image-935394\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1-1024x475.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1-300x139.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1-768x357.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1-240x111.jpg 240w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-talk-1.jpg 1400w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<p>In fact, TLA+ has been adopted for industrial use at semiconductor makers, companies that build distributed and database systems, other tech companies, and in more mainstream applications like payment systems in retail stores. It\u2019s likely that some applications aren\u2019t made public\u2014most companies don\u2019t publicly discuss their engineering process or proprietary technology.<\/p>\n\n\n\n<p>That\u2019s where the foundation comes in. A formal system for contributing to the tools and defining their future direction may spawn additional collaboration among engineers and facilitate commercial adoption. The foundation will create a steering committee, similar to other panels that look after public domain programming languages like C or <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/jcp.org\/en\/participation\/committee\" target=\"_blank\" rel=\"noopener noreferrer\">Java<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.&nbsp;<\/p>\n\n\n\n<p>\u201cI would hope that the new stewards make more subtractions than additions to the language, to remove some things that aren\u2019t needed,\u201d Lamport said.&nbsp;<\/p>\n\n\n\n<p>Now 82 years old and nearing retirement, Lamport also hopes the foundation gets TLA+ closer to the mainstream of industrial and academic discussion.<\/p>\n\n\n\n<p>\u201cTLA+ is never going to be as popular as Java. And I\u2019d be happy if someone else made it better at helping engineers think more mathematically,\u201d Lamport says. \u201cThe ultimate goal is to get engineers to think rigorously at a higher level about what they are doing.\u201d<\/p>\n","protected":false},"excerpt":{"rendered":"<p>TLA+ is a high level, open-source, math-based language for modeling computer programs and systems\u2013especially concurrent and distributed ones.&nbsp;It comes with tools to help eliminate fundamental design errors, which are hard to find and expensive to fix once they have been embedded in code or hardware.&nbsp; The TLA language was first published in 1993 by the [&hellip;]<\/p>\n","protected":false},"author":42183,"featured_media":936024,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[1],"tags":[],"research-area":[13561,13547],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[243984],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-935385","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-research-blog","msr-research-area-algorithms","msr-research-area-systems-and-networking","msr-locale-en_us","msr-post-option-blog-homepage-featured"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"<img width=\"960\" height=\"540\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-960x540.jpg\" class=\"img-object-cover\" alt=\"Leslie Lamport headshot in front of blurred code\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-960x540.jpg 960w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-300x169.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1024x576.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-768x432.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1066x600.jpg 1066w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-655x368.jpg 655w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-343x193.jpg 343w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-240x135.jpg 240w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-640x360.jpg 640w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1-1280x720.jpg 1280w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2023\/04\/leslie-lamport-headshot-1400x768-dark-1.jpg 1400w\" sizes=\"auto, (max-width: 960px) 100vw, 960px\" \/>","byline":"","formattedDate":"April 24, 2023","formattedExcerpt":"TLA+ is a high level, open-source, math-based language for modeling computer programs and systems\u2013especially concurrent and distributed ones.&nbsp;It comes with tools to help eliminate fundamental design errors, which are hard to find and expensive to fix once they have been embedded in code or hardware.&nbsp;&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/935385","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/42183"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=935385"}],"version-history":[{"count":10,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/935385\/revisions"}],"predecessor-version":[{"id":939300,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/935385\/revisions\/939300"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/936024"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=935385"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=935385"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=935385"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=935385"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=935385"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=935385"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=935385"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=935385"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=935385"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=935385"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=935385"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}