SysMoBench is a benchmark for evaluating generative AI's ability to formally model complex concurrent and distributed systems using TLA+. The benchmark uses four automated quality metrics: syntax correctness, runtime correctness, conformance via trace validation, and invariant correctness. Results show LLMs perform poorly on complex systems, with frequent syntax errors, hallucinated operators, and severe failures in temporal/liveness reasoning (41.9% liveness violations vs 8.3% safety violations). The author critiques the conformance metric for potentially biasing against good abstraction, notes the dataset is heavily skewed toward consensus protocols, and questions the value proposition for community contributions given current AI failure rates.
Sort: