Tim Dunbar

After hitting a wall with dataset construction, I'm doing what I should have done first — a formal literature review of the intersection of large language models and automated theorem proving.

In my last post, I collected 449 TLA+ files from GitHub and validated them down to 79 using basic structural checks — balanced brackets, module headers and footers. I reported that 52 of those 79 passed “TLC validation.”

Tonight I made significant progress on Symbolic, my project to train LLMs to generate TLA+ formal specifications from natural language descriptions. The key milestone: collecting and validating a dataset of real-world TLA+ specifications from GitHub.

Introducing Symbolic: a project to make formal verification accessible by translating natural language specifications into TLA+ using fine-tuned LLMs. This post explores the architecture, design decisions, and the mission to make formal methods as ubiquitous as unit testing.

A retrospective on eight years of professional and personal growth: completing a Master's in Computer Science at Georgia Tech, advancing to Director of Data Engineering, and pivoting toward AI architecture, formal methods, and quantum computing applications.

---

---

---

---

---