Lightnews — Scholar-powered news

lmstr.bsky.social @lmstr.bsky.social · Aug 21

2025 and progress bars continue to be a hard problem.

lmstr.bsky.social @lmstr.bsky.social · Aug 14

Building MCP servers is the perfect excuse to level up your input validation and user documentation. 😄

lmstr.bsky.social @lmstr.bsky.social · Aug 12

🏆 Winners of the first-ever #ai meets #tlaplus challenge:

🥇 From code to TLA+ specs, automatically.
🥈 Grammar-constrained AI that speaks TLA+.
🥉 Generating correct Rust from TLA+ specs.

Full details 👉 foundation.tlapl.us/challenge

GenAI-accelerated TLA+ challenge

🏆 Announcement: Winners of the 2025 TLAi+ Challenge The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the winners of the first GenAI-accelerated TLA+ Challenge—an open call for...

foundation.tlapl.us

2 1

lmstr.bsky.social @lmstr.bsky.social · Jun 26

Für diese Folge hätte mein Ambiente nicht besser sein können.

cid:704998CA-8594-4068-8AD2-738B9AE62CC9

lmstr.bsky.social @lmstr.bsky.social · Jun 26

Amazing how companies you've been giving money to for months suddenly no longer get your name right. Is this the result of too much vibe coding at Hertz?

lmstr.bsky.social @lmstr.bsky.social · Jun 5

Technically, it was NVIDIA who sponsored my work on TLC+LLMs.

2

lmstr.bsky.social @lmstr.bsky.social · Jun 3

More on why syntax has at least become a red herring: bsky.app/profile/hill...

Hillelogram @hillelwayne.com · Jun 3

Wow LLMs are pretty good at reading and explaining TLA+ error traces (and syntax errors). This could be real big for learners

Claude also did a great job of converting a spec from using 1 server to using N servers, an annoying bit of finicky boilerplate it handled well

lmstr.bsky.social @lmstr.bsky.social · Jun 3

Controversial take: The rejection of this Quint-related proposal (github.com/strimzi/prop...) suggests that people's real challenge with TLA+ isn't its syntax—it's the semantics.

github.com

1

lmstr.bsky.social @lmstr.bsky.social · May 30

Cheng is a long-time TLA+ expert. There is still lots to do to really democratize TLA+ with AI.

Reposted

Heidi Howard @heidihoward.bsky.social · May 27

It's wonderful to be writing again at Decentralized Thoughts! This time focusing on how we can tie together the messy reality of real-world distributed system to the elegant formal models we often use instead for reasoning about correctness. decentralizedthoughts.github.io/2025-05-23-s...

Reasoning about Distributed Protocols with Smart Casual Verification

Here at decentralized thoughts, we spend a lot of time reasoning about distributed protocols. Often, we focus on solving distributed consensus, personally it’s my favorite CS problem, but it’s also fa...

decentralizedthoughts.github.io

1 11

lmstr.bsky.social @lmstr.bsky.social · May 22

I scratched my own itch and got the MCP server launching directly from within my VSCode extension. Implementation at: github.com/tlaplus/vsco...

Expose TLA+ language model tools via Model Context Protocol (MCP) server by lemmy · Pull Request #379 · tlaplus/vscode-tlaplus

Add support for the Model Context Protocol (MCP) which enables TLA+ language model tools to be used by editors that implement MCP but don't support VS Code's native LanguageModelTool API (c...

github.com

Reposted

Heidi Howard @heidihoward.bsky.social · May 20

It's smart casual verification (like the dress code) instead of causal verification but still it's fab to see our recent NSDI paper featured in the @msftresearch.bsky.social Research Focus.

Microsoft Research @msftresearch.bsky.social · May 8

In this issue: New research on compound AI systems and causal verification of the Confidential Consortium Framework; release of Phi-4-reasoning; enriching tabular data with semantic structure, and more: msft.it/6012SVNCj

1 1 2

lmstr.bsky.social @lmstr.bsky.social · May 15

foundation.tlapl.us/blog/2025-05...

May 2025 Monthly Development Update

This is the TLA⁺ Foundation monthly development update (subscribe via RSS). Here we summarize the past month of development for the benefit of Foundation patrons and interested members of the communit...

foundation.tlapl.us

1

lmstr.bsky.social @lmstr.bsky.social · May 15

Related: www.reddit.com/r/mcp/commen...

How we built open extensibility into VS Code’s agent mode with MCP

www.reddit.com

1

lmstr.bsky.social @lmstr.bsky.social · May 13

"Je n’ai fait cette lettre-ci plus longue que parce que je n’ai pas eu le loisir de la faire plus courte." Pascal

1

lmstr.bsky.social @lmstr.bsky.social · May 13

As someone building a VSCode extension for #TLAplus, I have some questions about #VSCode, #Cursor, and #MCP. Would appreciate any insights!
🔗 forum.cursor.com/t/support-la...
🔗 github.com/microsoft/vs...

2 1

Reposted

A. Jesse Jiryu Davis @emptysqua.re · May 9

My notes from the 2025 TLA+ Community Event emptysqua.re/blog/2025-tl...

Jesse's 2025 TLA+ Community Event Notes

A one-day conference about temporal logic.

emptysqua.re

2 4

Reposted

Galois @galoisinc.bsky.social · May 8

What actually works when selling formal methods in industry?

What doesn't?

The way Galois Principal Scientist @m-dodds.bsky.social sees it, many FM projects don’t pencil out not because clients are irrational, but because the cost/benefit tradeoffs don’t make sense.
www.galois.com/articles/wha...

4 4

lmstr.bsky.social @lmstr.bsky.social · May 6

We were busy recording all the talks so you can watch them within 36 hours after the event at conf.tlapl.us/2025-etaps/ 😊

2025 - TLA+ Community Event :: TLA+ Community Event & Conference

conf.tlapl.us

3

lmstr.bsky.social @lmstr.bsky.social · May 6

🔧 GenAI-Accelerated #TLAplus Challenge is live!
Use GenAI to enhance TLA⁺ specs, tools, or workflows.
Submit your project for a chance to win a prize.
Details: foundation.tlapl.us/challenge/in...

GenAI-accelerated TLA+ challenge

The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the GenAI-accelerated TLA+ challenge—an open call for submissions that explore the intersection of TLA+ and generative AI. Thi...

foundation.tlapl.us

4 3

Reposted

Murat (Distributolog) @muratdemirbas.bsky.social · Feb 26

[new blog post]

Smart Casual Verification of the Confidential Consortium Framework (NSDI'25)

muratbuffalo.blogspot.com/2025/02/smar...

Smart Casual Verification of the Confidential Consortium Framework

This paper (NSDI'25) applies lightweight formal methods (hence the pun "smart casual" in contrast to formal attire) to the Confidential Con...

muratbuffalo.blogspot.com

1 7

Reposted

Heidi Howard @heidihoward.bsky.social · Feb 27

A big thank you to @muratdemirbas.bsky.social for covering our upcoming NSDI paper on his blog. The paper documents our adventures with “smart casual verification”, combining formal specification and model checking with validation of real execution traces from the Confidential Consortium Framework

Murat (Distributolog) @muratdemirbas.bsky.social · Feb 26

[new blog post]

Smart Casual Verification of the Confidential Consortium Framework (NSDI'25)

muratbuffalo.blogspot.com/2025/02/smar...

Smart Casual Verification of the Confidential Consortium Framework

This paper (NSDI'25) applies lightweight formal methods (hence the pun "smart casual" in contrast to formal attire) to the Confidential Con...

muratbuffalo.blogspot.com

2 10

lmstr.bsky.social @lmstr.bsky.social · Jan 4

Hard to answer without knowing what the book is about?

lmstr.bsky.social @lmstr.bsky.social · Dec 5

As Jack's blog post points out, Fizzbee is programming. Therefore, it shares more similarities with comparable approaches, such as P.

1 1

lmstr.bsky.social @lmstr.bsky.social · Dec 5

My comparison stops at: Both allow you to define a state machine, check invariants and temporal properties, and come with a model checker.

1 1