Show HN: TLA+ AutoRepair (with GPT-4) to fix formal specs and understand them

4 points

3 years ago

TLA+ is a language for formal specification. It can be used to formally verify algorithms and mathematical theorems. Companies like AWS use it for verifying mission-critical parts of systems like S3.

The challenge is that TLA+ and formal specifications have a steep learning curve. This tool can aid in overcoming this obstacle at the outset.

TLA+ AutoRepair is used to repair/self-heal formal specifications with GPT-4 in a loop, with or without human intervention.

Given a TLA+ specification (.tla file) and a model to check (.cfg), the application will go through each error, send it to GPT-4 (or specified model), and fix all errors. Finally, it will document the code to make it more readable.

Example Command: python3 autorepair.py Test_Specs/Counter.tla --model=gpt-4

1 comment