Rubik's Snake — Formally Verified
Coq (Rocq) and TLA+ specifications of the Rubik’s Snake state space — 4^23 configurations, formally
TLA+
ChatTLA+ Dataset
The dataset release for the ChatTLA+ paper — SFT corpus and benchmark for TLA+ spec generation, posted anonymized for blind review.
ChatTLA+
Presentation on using LLMs for TLA+ formal specification generation and verification.
TLA+ Model of a Walk-In Oven
A formal TLA+ specification of a walk-in industrial oven with a focus on safety interlocks.
TLA+ Model of a Laptop
A formal TLA+ specification modeling a laptop’s power states, battery, lid, thermals, and auto-suspend.
TLA+ Model of Dexcom G7
A formal TLA+ specification of the Dexcom G7 continuous glucose monitor’s behavior and safety properties.
TLA+ Formal Generation
Early exploratory repo for generating TLA+ specs from natural-language requirements with an LLM, with a TLC harness wired in. The scaffold that eventually grew into ChatTLA+.
Researcher
Research on TLA+ and fine-tuning open-source LLMs for formal methods.
Connect 4 Game Engine
A Chess engine-esque Connect 4 analyzer
Web Based TLA+ Microwave
An interactive microwave in the browser to learn TLA+
Software Engineer
Implemented a web-based visualization and demo application for TLA+ using Spring Boot and Vaadin.