Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- Gotta love TLA+
I wonder if anyone has worked on porting it to Lean and making tactics for it
by vatsachak - 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
- 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
- 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 questionsby letFunny
- 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.)