William Schultz

@JAldrichPL The model checking problem formulation (e.g. checking invariant of a transition system) may be slightly tangential to the program analysis/verification setting you are referring to, but my intuition is that the fundamentals are transferrable to a reasonable degree.

@JAldrichPL Elaborated on better by Bradley/Manna (theory.stanford.edu/~arbrad/papers…)

Verification folks: when building a tool like Dafny or Verus, is there a strong technical reason to prefer backwards reasoning/weakest preconditions vs. forward reasoning/symbolic execution? Or are they more or less equivalent and it's just a matter of taste?

@MarcJBrooker I think it's kind of equivalent to forcing one big global read at the end of any serial execution (i.e. to validate the actual DB state). This "write-specific serializability" notion in recent paper kind of makes practical use of a similar idea: wsdou.github.io/papers/2025-vl…

@MarcJBrooker Even without real-time guarantees, always felt like there could be a reasonable, alternate serializability definition that was something like "the state of the database after executing these transactions is equivalent to some serial execution".

Best of all, /dev/null is also serializable (but not strict serializable) under many academic and textbook definitions. jyu.dev/blog/why-dev-n…

Vol:18 No:12 → Design and Modular Verification of Distributed Transactions in MongoDB vldb.org/pvldb/vol18/p5…

@joshmpollock @its_bvisness @redblobgames @AndrewCMyers The idea was to possibly use something like Bluefish as a core visualization library, embedding its primitives in TLA+. Visualizations in the tool are basically just functions from “TLA+ protocol state”-> "raw SVG", so I was looking for some abstraction to sit in between.

@joshmpollock @its_bvisness @redblobgames I felt like simple libraries such as @AndrewCMyers Constrain.js were in the right direction, and I liked some of the higher level Bluefish primitives like “StackH/StackV”. Currently I just embed raw SVG primitives inside TLA+ in a semi-janky way: #L210-L310" target="_blank" rel="nofollow noopener">github.com/will62794/spec…

Was excited to check this out since it was retweeted by @redblobgames, but wow it is such a disappointment It's "declarative", but order matters (items in the diagram can't refer to future items) It's "reactive", but they don't provide a single example of a dynamic diagram

@joshmpollock @its_bvisness @redblobgames I'd be interested in any new iterations of Bluefish as well! Have looked around for nice "declarative"-ish visualization langs for describing protocol animations inside github.com/will62794/spec… (browser tool for interactively exploring TLA+ specs)

@its_bvisness @redblobgames Hey Ben! Thanks for checking out Bluefish and for your detailed feedback. As you've shown, the system has a lot of rough edges, especially around Refs. I haven't fixed them since I’m working on a second iteration of the system. My DMs are open if you’d like to chat more!

The protocol is formally specified and verified in TLA+, and, for fun, you can also take it for a spin in this interactive protocol visualization: will62794.github.io/spectacle/#!/h…

Consensus protocols are hard, and dynamic reconfiguration (replacing failed machines w/ new ones) is even trickier. I wrote about our use of formal methods in MongoDB to design a novel, "logless" reconfiguration protocol quickly and confidently. mongodb.com/company/blog/t…