Projects
Specula
An agentic system for finding deep bugs in concurrent and distributed system code. Specula generates and validates TLA+ specifications, uses model checking to discover violations, and reproduces confirmed findings in the implementation.
TLAPS-Bench
A benchmark for evaluating AI’s ability to write machine-checked proofs for the TLA+ Proof System. It supports both proof completion and proof construction from scratch, with reproducible evaluation and a public leaderboard.
SysMoBench
A benchmark for evaluating AI’s ability to formally model complex real-world systems. It measures whether generated TLA+ specifications are syntactically valid, executable, aligned with implementation behavior, and consistent with correctness properties.
System Intelligence Benchmark
A benchmark suite for evaluating LLMs and AI systems across computing-system capabilities, including systems education, artifact evaluation, formal modeling, verification, and operations.
[GitHub]