Heidi Howard

@heidiann360
123 Followers
76 Following
20 Posts
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. https://decentralizedthoughts.github.io/2025-05-23-smart-casual-verification/
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 famously one of the most difficult and subtle problems in distributed computing. Reasoning about distributed algorithms is hard at the...

great blog post "What Works (and Doesn't) Selling Formal Methods" -- properly focusing on the economics and on communicating what the results mean to a client. both of these are pretty significantly under-appreciated in the FM research community.

https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods

What Works (and Doesn't) Selling Formal Methods

Spamming TLA⁺ stuff today because I wanted to get that last post out before the publication date of this post: the May monthly development update! TLA⁺ Community Event talk recordings posted, a contest with a NVIDIA RTX 5090 as the grand prize, GraalVM native image builds, and a big focus on improving usability this month.

https://foundation.tlapl.us/blog/2025-05-dev-update/index.html

#TLAPlus

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 community. We will also highlight a good bug or small feature for prospective new contributors to look at! If your TLA⁺ contribution was missed, worry not - we publish monthly, so it’s easy to hop on the next train; open an issue here.

TLA+ Foundation
When your own employer refers to your research as “causal verification” instead of “smart casual verification”. Still it’s great to be included in the Microsoft Research Focus, even if they didn’t quite get the word play. https://www.microsoft.com/en-us/research/blog/research-focus-week-of-may-7-2025/
Research Focus: Reimagining compound AI systems, Phi-4-reasoning

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:

Microsoft Research
A quick history lesson in the sunshine before #NSDI25. Exciting to speaking about our paper on “smart casual verification” with #TLAplus and how we applied it to find and fix subtle bugs in our distributed system the Confidential Consortium Framework.

[new blog post]

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

https://muratbuffalo.blogspot.com/2025/02/smart-casual-verification-of.html

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

I can’t quite believe how excited I am to be attending my first in-person academic conference since the pandemic (due to covid, switched jobs, budget cuts etc). Boarding a plane across the pond like it’s 2019 again. Come say hi to real life me at SIGMOD
I’ll be at @emf next week if anyone is around. For those who are unfamiliar, EMF is a British hacker camp where people wear flaming hats, robotic monsters roam the earth (+ make cocktails) and schedule is available on teletext https://www.emfcamp.org
Electromagnetic Field

Electromagnetic Field is a non-profit UK camping festival for those with an inquisitive mind or an interest in making things.

Electromagnetic Field
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 https://jobs.careers.microsoft.com/global/en/job/1703375/Cambridge-Residency-Programme-–-Post-Doc-Researcher-Security-and-Privacy
Search Jobs | Microsoft Careers

truly one of the greatest achievements in the history of our species: a design doc for a student's implementation of MultiPaxos, expressed entirely using memes: https://students.washington.edu/finnb/finnb_cse452_lab3_design_doc.pdf (shared with permission)