alt.hn

6/30/2026 at 11:07:38 AM

Hunting a 16-year-old SQLite WAL bug with TLA+

 https://ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected

by peterparker204

7/3/2026 at 3:18:31 PM

TLA+ = formal language for modeling software above the code level and hardware above the circuit level by Leslie Lamport (of vector clock and Paxos fame, among other things.)

https://lamport.azurewebsites.net/tla/tla.html

by hackingonempty

7/3/2026 at 5:23:15 PM

So there's \in, \subseteq and probably many others that are written just like in Latex. Notably \cap and \cup were also copied from Latex, which describe the shape of the symbol instead of its meaning. But not \to, \mapsto, \Vee and \Wedge, they're written as ASCII art ->, |->, \/ and /\.

Then there's SUBSET, which means power set ... yeah. -_-

by mike_hock

7/4/2026 at 9:33:15 AM

If the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".

by igornotarobot

7/4/2026 at 10:44:06 AM

No, I just find the inconsistent syntax annoying, but it turns out most things have alternative Latex-style spellings. I just went by their examples.

by mike_hock

7/3/2026 at 7:26:02 PM

Author of the article here. I am surprised to see the post was submitted and made it to the front page! Happy to answer any questions

by letFunny

7/4/2026 at 12:26:41 AM

You’re in a desert walking along in the sand when all of the sudden you look down, and you see a tortoise, it’s crawling toward you. You reach down, you flip the tortoise over on its back. The tortoise lays on its back, its belly baking in the hot sun, beating its legs trying to turn itself over, but it can’t, not without your help. But you’re not helping. Why is that?

by sennalen

7/4/2026 at 2:34:54 AM

Because that would reverse flipping it over the first time, and our universe's physics are not reversible. Thermodynamics demands the turtle stay flipped.

by Groxx

7/4/2026 at 3:21:59 AM

What’s a tortoise?

by _doctor_love

7/4/2026 at 5:49:28 AM

A turtle-like animal that only lives on land.

by erikerikson

7/4/2026 at 5:16:51 AM

You know what a turtle is? Same thing, Leon.

by wowczarek

7/3/2026 at 10:18:21 PM

Thanks for the nice article. The SQLite docs that explain this bug are emphatic about how utterly rare, even irreproducible it is. How, then, was it found, one wonders?

by buggymcbugfix

7/4/2026 at 2:46:07 AM

We found it at Tailscale and bought an enterprise support contract from SQLite to debug it for us. Worth every penny.

We should probably blog about it.

by bradfitz

7/4/2026 at 3:23:52 AM

What mission critical purpose does sqlite provide at Tailscale exactly? Why use it at all?

by doctorpangloss

7/4/2026 at 9:23:17 AM

sqlite is useful everywhere CSV files are useful but you'd like them to have more data integrity and faster updates. sqlite can replace some uses of MySQL, but more commonly it replaces fopen. https://sqlite.org/whentouse.html

by inigyou

7/4/2026 at 6:53:57 AM

It's in Chrome, Firefox, Safari, Windows 10, macOS because it efficiently solves a huge number of use cases while giving plenty of headroom for flexible querying.

If you have data more complicated than a single CSV or tab-separated text file that you will only ever process in sequential order, and you don't need inter-process interaction, you should be asking why not use SQLite.

by akoboldfrying

7/3/2026 at 10:41:56 PM

My guess is that they noticed something was not quite right when inspecting the code and then tested their hypothesis manually to see if it was actually a real bug.

Something similar happened to me when I was working on some code that should clear the state and, by inspection, I noticed some field was not properly cleared under specific circumstances. Then I tested the hypothesis and indeed found a bug. Sometimes intuition and guessing is what it takes.

by letFunny

7/3/2026 at 8:16:11 PM

"to prevent multiple from" seems to be missing a word.

by stevekemp

7/4/2026 at 3:19:59 AM

[dead]

by keynha

7/3/2026 at 11:09:42 PM

I don't like the title. The article actually describes the process of proving that dqlite does not have the same bug as SQLite, using a TLA+ specification. The SQLite bug fix was entirely separate from what is described here.

by romaaeterna

7/3/2026 at 7:07:29 PM

Gotta love TLA+

I wonder if anyone has worked on porting it to Lean and making tactics for it

by vatsachak

7/3/2026 at 8:26:35 PM

i am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx.

Also congratulations to the author, I'll try and reproduce this over the weekend.

by another_twist

7/4/2026 at 3:51:22 AM

This is so cool and I wonder how effective it would be using this technique when using LLMs to generate code. Have the llm generate code and a TLA+ model. Use the TLA+ model as the test bed of the code (instead of writing tests in the original language).

by mempko

7/4/2026 at 12:06:22 PM

[flagged]

by disclaimer8

7/3/2026 at 8:57:52 PM

[flagged]

by mateenah

7/3/2026 at 9:26:14 PM

[flagged]

by tomiow

7/3/2026 at 9:27:29 PM

wut

by alunchbox

6/30/2026 at 11:07:38 AM

[flagged]

by peterparker204

7/3/2026 at 9:15:41 PM

[flagged]

by hnloser