@lmstr.bsky.social
lemmster.de
@lemmster, @lmstr, or @lemmy elsewhere
@lemmster, @lmstr, or @lemmy elsewhere
2025 and progress bars continue to be a hard problem.
August 21, 2025 at 10:21 PM
2025 and progress bars continue to be a hard problem.
Building MCP servers is the perfect excuse to level up your input validation and user documentation. 😄
August 14, 2025 at 12:39 AM
Building MCP servers is the perfect excuse to level up your input validation and user documentation. 😄
🏆 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
🥇 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
August 12, 2025 at 10:04 PM
🏆 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
🥇 From code to TLA+ specs, automatically.
🥈 Grammar-constrained AI that speaks TLA+.
🥉 Generating correct Rust from TLA+ specs.
Full details 👉 foundation.tlapl.us/challenge
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?
June 26, 2025 at 5:24 PM
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?
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
June 3, 2025 at 6:19 PM
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.
Reposted
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
May 27, 2025 at 9:36 AM
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...
Reposted
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.
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
May 20, 2025 at 1:35 PM
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.
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...
🔗 forum.cursor.com/t/support-la...
🔗 github.com/microsoft/vs...
May 13, 2025 at 5:17 PM
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...
🔗 forum.cursor.com/t/support-la...
🔗 github.com/microsoft/vs...
Reposted
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
May 9, 2025 at 2:24 AM
My notes from the 2025 TLA+ Community Event emptysqua.re/blog/2025-tl...
Reposted
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...
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...
May 8, 2025 at 4:32 PM
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...
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...
🔧 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...
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
May 6, 2025 at 12:36 PM
🔧 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...
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...
Reposted
[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 (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
February 26, 2025 at 8:02 PM
[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 (NSDI'25)
muratbuffalo.blogspot.com/2025/02/smar...
Reposted
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
[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 (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
February 27, 2025 at 10:20 AM
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
Save the date! The TLA+ Community Event 2025 will take place on May 4, 2025, in Hamilton, Canada. This marks a first for our academic conference, as it will be held outside Europe for the very first time.
conf.tlapl.us/2025-etaps/ #tlaplus
conf.tlapl.us/2025-etaps/ #tlaplus
2025 - TLA+ Community Event :: TLA+ Community Event & Conference
conf.tlapl.us
November 26, 2024 at 5:26 PM
Save the date! The TLA+ Community Event 2025 will take place on May 4, 2025, in Hamilton, Canada. This marks a first for our academic conference, as it will be held outside Europe for the very first time.
conf.tlapl.us/2025-etaps/ #tlaplus
conf.tlapl.us/2025-etaps/ #tlaplus