Formal Methods

A statically-typed compiled language for safety-critical embedded systems, with Z3-verified contracts and self-healing runtime blocks

Coq (Rocq) and TLA+ specifications of the Rubik’s Snake state space — 4^23 configurations, formally

A formal TLA+ specification of a walk-in industrial oven with a focus on safety interlocks.

A formal TLA+ specification modeling a laptop’s power states, battery, lid, thermals, and auto-suspend.

A formal TLA+ specification of the Dexcom G7 continuous glucose monitor’s behavior and safety properties.

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+.

Research on TLA+ and fine-tuning open-source LLMs for formal methods.

An interactive microwave in the browser to learn TLA+

The formal methods language