#tla — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #tla, aggregated by home.social.
-
Next week I am going to Tokyo to give a presentation at the ABZ 2026 conference. Title: “Identifying Design Flaws in a Lock-Free Task Pool with TLA+”. It is an “application in industry” paper, I will upload it and the slides a bit later
We specified an algorithm with the simple goal of confirming its correctness, and instead found numerous issues without an obvious way to fix them (if it is even possible). Finding this early saved us huge amount of time and resources, and i think the result is quite a bit unusual
ABZ is my favorite conference, it is about state-based #formalmethods like Alloy, Event-B and #TLA+. The papers are always interesting, and each conference has a “case study” track, in which practitioners specify the given system using any state-based method they want and describe the results and their observations. This time the system is an autonomous planetary rover
Side note: my first trip abroad was back in 2014, and it was also to speak at ABZ :) I even met and spoke with Jean-Raymond Abrial!
-
Can #LLMs model real-world systems in TLA+? 🤔 Oh sure, because who wouldn't want a linguistically confused #AI applying #logic it doesn't truly comprehend to complex systems modeling? 🙄 Next up: teaching your cat to do your taxes! 🐱💼
https://www.sigops.org/2026/can-llms-model-real-world-systems-in-tla/ #TLA+ #complexsystems #catstaxes #HackerNews #ngated -
Can LLMs model real-world systems in TLA+?
https://www.sigops.org/2026/can-llms-model-real-world-systems-in-tla/
#HackerNews #LLMs #TLA #realworldsystems #modeling #technews
-
Применяем TLA+ на практике
Привет, Хабр! Меня зовут Сергей, я работают в компании InfoWatch разработчиком на продукте ARMA Стена (NGFW). Подробнее о том, что такое ARMA Стена, можно прочитать тут . В этой статье я хочу поделиться опытом применения метода формальной верификации в решении практической бизнес-задачи. Сразу оговорюсь, что в статье используется TLA+, без введения в инструмент, чтобы не увеличивать объём статьи. Подробнее про инструмент вы можете почитать на сайте создателя , тут и тут . Необходимые объяснения даются по ходу изложения. Статья состоит из двух частей: 1) Что такое формальная верификация и где она применятся 2) Решение бизнес-задачи в NGFW Верифицировать статью
-
Применяем формальные методы к чейнкодам Hyperledger Fabric: кейс BaseToken
Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Речь пойдет о верификации смарт-контракта BaseToken в Hyperledger Fabric с помощью метода проверки моделей.
https://habr.com/ru/companies/pt/articles/993688/
#Hypeledger_Fabric #смартконтракты #чейнкод #формальная_верификация_криптовалют #model_checking #tla+ #блокчейн #hlf
-
🚀 "Proving liveness with TLA" or how to make watching paint dry sound exciting! 🎨 Dive into a labyrinth of tech jargon that promises something will *eventually* happen, just like your New Year's resolutions! 📅😂
https://roscidus.com/blog/blog/2026/01/01/tla-liveness/ #ProvingLiveness #TLA #TechJargon #ExcitingReads #NewYearsResolutions #LabyrinthOfTech #HackerNews #ngated -
Experiences using the #TLA Toolbox with TLAPS to prove liveness for the Xen vchan protocol: https://roscidus.com/blog/blog/2026/01/01/tla-liveness/
-
CPU
(Central Processing Unit)GPU
(Graphics Processing Unit)TPU
(Tensor¹ Processing Unit)And I need an
HPU
(Hype Processing Unit).Robert McNamara wrote about the Fog of War;
this is the Fog of November²...From the BBC:
The contradiction at the heart of the trillion-dollar AI race
<https://www.bbc.com/news/articles/cvgvynlxqdyo>_________
¹ I can hear the conversation:
"Yes! tensor! it's like a vector on steroids, right?"
² Today's month being the month preceding winter
(in this part of the world). -
I’m very close to finishing another #edh deck, but once I’m done I’m going to have to revamp my Tazri Allies deck. #mtgcommander #mtg #magicthegathering #tla
-
Update ! Page d'accueil https://PoLiTiPeT.fr : ajout de sel, dyn et fédi en plein milieu du menu.
Toutes les listes / vues / présentations sont maintenant accessibles directement et "explicitement".
Un tas de #TLA, un poil cryptique, mais tout est disponible depuis un seul endroit 🎉
-
Yesterday I had added some #TLA+ specs to the Confluence back at work and was very surprised when I saw some syntax highlighting, all definitions and their references were clearly marked by some color.
What is interesting is that Code block on Confluence does not have TLA+ in the drop-down menu of supported languages. It is possible that it just incorrectly applies some highlighting based on the code analysis, but the result looks a bit too good for this to be true.
Mystery.
-
Aviation weather for Teller airport (USA) is “SPECI PATE 242134Z AUTO 35009KT 10SM SCT013 OVC025 03/01 A2966 RMK AO2 TSNO” : See what it means on https://www.bigorre.org/aero/meteo/pate/en #teller #usa #tellerairport #pate #tla #metar #aviation #aviationweather #avgeek #airport vii3
-
Aviation weather for Teller airport (USA) is “SPECI PATE 242134Z AUTO 35009KT 10SM SCT013 OVC025 03/01 A2966 RMK AO2 TSNO” : See what it means on https://www.bigorre.org/aero/meteo/pate/en #teller #usa #tellerairport #pate #tla #metar #aviation #aviationweather #avgeek #airport vl
-
YIL:
Yesterday I Learned
that Nebraska used to be known as NB before New Brunswick remained the sole nominee (in 1962 or thereabout).The occasion was an error in a US weather report about hurricane Erin bringing surge waves to Nebraska (spelled out in full).
(NC was badly affected indeed and NJ was also affected, possibly NY as well.)
-
Leslie Lamport, just what an attitude
#computerscience #lamport #arrogance #tla -
Here is a very nice experience report of conformance checking between #TLA+ specs and implementation, covering both test-case generation and trace checking: https://www.mongodb.com/company/blog/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs
There are a lot of links to other reports and papers, I recommend to check them out too.
-
How many runways can you see for Teller airport (USA) ? : The answer is on https://www.bigorre.org/aero/meteo/pate/en #teller #usa #tellerairport #pate #tla #airport #aviation #avgeek vl
-
Systems Correctness Practices at Amazon Web Services. Leveraging formal and semi-formal methods.
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/ -
-
-
