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.
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
As Language Learning Models (LLMs) are helping improve developer productivity, it might make sense to look at code from a higher perspective. The challenge is that TLA+ and formal specifications have a steep learning curve. This tool can aid in overcoming this obstacle at the outset.
- Clone the repo e.g. git clone https://github.com/kerberosmansour/TLA_AutoRepair.git
- Create a .env file in the folder and add your OpenAI Key.
- Run AutoRepair on a TLA+ Spec. Example Command: python3 autorepair.py Test_Specs/Counter.tla --model=gpt-4
- NOTE: There is a folder with TLA+ specifications that need repair.
- NOTE: The code, by default, will check if TLA+ is installed on your system. If not, it will attempt to install it for you in these locations:
- "Windows": "C:/Program Files/TLA+",
- "Darwin/MacOS": "/Users/Shared/TLA+",
- "Linux": "/usr/local/share/TLA+",
- NOTE: TLA+ requires Java.
- spec_name "The name of the TLA+ specification to check"
- --revert "Revert the specification to its previous state"
- --model "The name of the GPT model to use"
- --confirm "Ask for confirmation before each change"