Waterloo Formal Methods Lab (WatForm)

Benchmark consisting of Alloy models and English descriptions to test how well LLMs can generate Alloy Models

Web-based Dash+ visualization and interactive simulation

Integration testing for Dash translations to other languages

Scripts for creating the alloy-llm-benchmark

Testing of Alloy to TLA translator

Evaluation scripts for "Portus: Linking Alloy with SMT-based Finite Model Finding"

Fortress: Finite Model Finder for Many-Sorted First-Order Logic