Lmst

Применяем TLA+ на практике

Привет, Хабр! Меня зовут Сергей, я работают в компании InfoWatch разработчиком на продукте ARMA Стена (NGFW). Подробнее о том, что такое ARMA Стена, можно прочитать тут . В этой статье я хочу поделиться опытом применения метода формальной верификации в решении практической бизнес-задачи. Сразу оговорюсь, что в статье используется TLA+, без введения в инструмент, чтобы не увеличивать объём статьи. Подробнее про инструмент вы можете почитать на сайте создателя , тут и тут . Необходимые объяснения даются по ходу изложения. Статья состоит из двух частей: 1) Что такое формальная верификация и где она применятся 2) Решение бизнес-задачи в NGFW Верифицировать статью

https://habr.com/ru/companies/infowatch/articles/1003382/

#формальная_верификация #tla+ #python #ngfw #ARMA

Pathological Digital Affection Personal Display Avoidance Public Demand Assistant #PDA #TLA

Learn TLA+ by example, from the Transcendental Hillel Wayne (which is how I’d imagine his Marvel series would be titled).

#tla #formalMethods #math

https://tlabyexample.com/

Применяем формальные методы к чейнкодам 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

Proving Liveness with TLA

https://roscidus.com/blog/blog/2026/01/01/tla-liveness/

#HackerNews #Proving #Liveness #TLA #FormalMethods #DistributedSystems

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/

A screenshot of the TLA Toolbox being used to verify a protocol. A bright Spec Status indicator glows a friendly green, confirming that the proof has been successfully parsed (tactfully, it remains silent about its validity).

TLA+ Modeling Tips

http://muratbuffalo.blogspot.com/2025/12/tla-modeling-tips.html

#HackerNews #TLA+ #Modeling #Tips #TLA+ #Modeling #Software #Formal #Methods #Software #Engineering #System #Design

I walked into a big-box retailer two days in a row and noticed that #mtg #tla Commander Bundles are plentiful at $109 (an incorrect, lower price was on the shelf, and the in-store price checker said they were out of stock.) You couldn’t buy through the app, you had to go in person. Point is anyone buying or reselling over that amount is losing their shirt. #mtgcommander #magicthegathering

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).

#AI
#ArtificialIntelligence
#FifthGeneration
#Hype
#Seasons
#TLA

@fatsam
#TLA

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

Magic: the Gathering card United Front {X}{X}{w} Sorcery Create X 1/1 white Ally creature tokens, then put a +1/+1 counter on each creature you control.

#TIL si tu savais pas ce que ce #TLA veut dire

Photo "corporate", à gauche une femme métis à lunettes qui sourit à son ordinateur portable, à droite le texte :

Today
I
Learned

texte en blanc, les premières lettres en majuscules orange, le tout sur fond rose brique

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.

@rl_dane
DAW is a #TLA I'm not familiar with, but i've used #Audacity a bit. Perhaps that is more for fiddling with what you want to do after you've done it?
#Ardour I've heard of, and #Tenacity was an alternative to Audacity.
All #FLOSS