Show HN: TLA+ AutoRepair (with GPT-4) to fix formal specs and understand them https://ift.tt/8jSsyiR

Show HN: TLA+ AutoRepair (with GPT-4) to fix formal specs and understand them 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 https://ift.tt/OGeAd0q July 25, 2023 at 12:43AM

Komentar

Posting Komentar

Postingan populer dari blog ini

Show HN: Interactive exercises for GNU grep, sed and awk https://ift.tt/OxeFwah

Show HN: Interactive exercises for GNU grep, sed and awk Hello! For the past few months, I've been using a Python framework called Textual to create TUI apps for interactive exercises. Released the app for GNU awk earlier today, so thought I'd create a post here. If you already know how to manage Python packages, you can use the following command to get all the three apps: pip install grepexercises sedexercises awkexercises `pipx` should also work, but I haven't tested it. The GitHub repo has the source code as well as more detailed installation instructions. You can use alternative CLI tools to solve these exercises as well. For example, Perl instead of GNU awk or ripgrep instead of GNU grep and so on. Hope you find these TUI apps useful. I'd highly appreciate your feedback. Happy learning :) https://ift.tt/Hp9kFEi August 17, 2023 at 05:13PM
Baca selengkapnya

Show HN: Create demos & guides just with a simple prompt https://ift.tt/HfWo3mz

Show HN: Create demos & guides just with a simple prompt Teams often create demos & guides on a daily basis. But creating them is time consuming and needs a lot of effort. From content to the branding, customizations, and many more - they are not something you would want to do on a daily basis. Enter Fable. Purpose built for teams in marketing, sales & customer success. Fable is apt for engaging visitors, closing deals faster, and onboarding your users quickly. https://ift.tt/IVCbkiG October 17, 2024 at 08:32PM
Baca selengkapnya