tlafmt

A formatter for TLA+ specs.

It looks like this:

Add(t, k, v) == \* Using transaction t, add value v to the store under key k.
    /\ t \in tx
    /\ snapshotStore[t][k] = NoVal
    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]
    /\ written' = [written EXCEPT ![t] = @ \union {k}]
    /\ UNCHANGED << tx, missed, store >>

Some TLA specs are hand-crafted works of art - but not all of them - this tool is for those ugly specs!

• Optimises for easily readable output.
• Consistent formatting across different teams and authors.
• Helpful but not forceful - small tweaks, not big rewrites!
• Fast rendering - suitable for "format on save" in interactive editors.

Install

Download pre-built binaries from the releases page.

Or if you have Rust installed, compile it yourself: cargo install tlafmt.

Usage

Format a file and print the formatted result to stdout:

% tlafmt bananas.tla

Or overwrite the input file with the formatted result:

% tlafmt --in-place bananas.tla

To check if a file is formatted and return an error if it isn't, use --check:

% tlafmt --check bananas.tla
# Exits code 3 for unformatted code.

Check out the --help text too.

Style

This formatter doesn't aim to enforce a prescriptive, universal style across the whole spec. Instead it aims to improve consistency by making small changes, respecting the general style of the input spec.

Formatting is being iterated on - please report any undesirable rendering as an issue.