Heidi Howard
@heidihoward.bsky.social
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...
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.
Reposted by Heidi Howard
🔧 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...
A quick history lesson in the sunshine before NSDI. Exciting to speaking about our paper on “smart casual verification” with TLA+ and how we applied it to find subtle bugs in our distributed system, the Confidential Consortium Framework.
April 28, 2025 at 6:49 AM
A quick history lesson in the sunshine before NSDI. Exciting to speaking about our paper on “smart casual verification” with TLA+ and how we applied it to find subtle bugs in our distributed system, the Confidential Consortium Framework.
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
BFT as a poem (thanks to AI):
In webs of nodes where chaos plays, Byzantine whispers cloud the ways.
Yet trust persists, through trials deep, Consensus wakes where doubts would creep.
Resilient minds, a truth refined,
Order from discord, tightly aligned.
In webs of nodes where chaos plays, Byzantine whispers cloud the ways.
Yet trust persists, through trials deep, Consensus wakes where doubts would creep.
Resilient minds, a truth refined,
Order from discord, tightly aligned.
January 28, 2025 at 9:30 PM
BFT as a poem (thanks to AI):
In webs of nodes where chaos plays, Byzantine whispers cloud the ways.
Yet trust persists, through trials deep, Consensus wakes where doubts would creep.
Resilient minds, a truth refined,
Order from discord, tightly aligned.
In webs of nodes where chaos plays, Byzantine whispers cloud the ways.
Yet trust persists, through trials deep, Consensus wakes where doubts would creep.
Resilient minds, a truth refined,
Order from discord, tightly aligned.
Interesting workshop and a lovely community, would very much recommend!
The PaPoC workshop is once again accepting submissions on distributed consistency. Deadline 15 January papoc-workshop.github.io/2025/cfp.html
Call for Papers
The 12th Workshop on Principles and Practice of Consistency for Distributed Data
papoc-workshop.github.io
December 15, 2024 at 4:04 PM
Interesting workshop and a lovely community, would very much recommend!
We’re looking for two postdocs to join us at Azure Research. Please help to get the word out to final year phd students and early careers researchers in the areas of security & privacy, formal verification, systems, architecture and/or cryptography
Cambridge Residency Programme – Post Doc Researcher Security and Privacy in Cambridge, Cambridgeshire, United Kingdom | Research, Applied, & Data Sciences at Microsoft
Apply for Cambridge Residency Programme – Post Doc Researcher Security and Privacy in Cambridge, Cambridgeshire, United Kingdom | Research, Applied, & Data Sciences at Microsoft
jobs.careers.microsoft.com
April 15, 2024 at 10:39 AM
We’re looking for two postdocs to join us at Azure Research. Please help to get the word out to final year phd students and early careers researchers in the areas of security & privacy, formal verification, systems, architecture and/or cryptography