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: My Book Bulletproof TLS and PKI (Second Edition) Is Out https://ift.tt/5PZ9mxF

Show HN: My Book Bulletproof TLS and PKI (Second Edition) Is Out Hello HN. I am excited to share with you my new book, Bulletproof TLS and PKI. I've worked in this space since the very early days (think SSLv2), always frustrated with the fact that the field is vast but the documentation poor. That first led me to create SSL Labs (which ended up being very popular) and then the first edition of my book (in 2014), where I aimed to cover everything a curious person needed to know about SSL/TLS and PKI. Most importantly, it's a very practical book that you can use to just learn what you need at that moment. The second edition (just out) adds coverage of TLS 1.3. I publish two chapters as a separate (and free) OpenSSL Cookbook. There's another free sample chapter as well. The best part of Bulletproof TLS and PKI is that it's a living book. There's nothing worse than obsolete documentation! Because none of the traditional publishers were interested in that sort of thing,
Baca selengkapnya