The Berkeley Function Calling Leaderboard checks only the final state, so models that ask before deleting get penalized; 260 of 734 reference turns act destructively without confirmation. CAREFUL-Bench replays runs and flags unrequested destructive calls, duplicate writes and surplus steps. Across 11 open models the ranking holds, but the leader loses 14.0 points and surplus steps use up to 28% of input tokens. The best model completes only six of 576 conversations needing confirmed destructive actions.
TLAPS-Bench gives AI agents a harness for writing machine-checked correctness proofs of system designs in TLA+, a language for specifying how systems behave. It holds 265 proof targets from 95 real-world specifications, including cache coherence, Byzantine consensus and write-ahead logs. Testing Codex with GPT models on 70 targets across 12 specifications, the top model, GPT-6.1 Sol (max), proved 31, or 44.3%. Agents also proved properties of important specifications that were never proved before.
SessionFarmer turns chat-driven coding sessions and their commits into self-contained tasks with a container, task statement, rubrics and unit tests. Its open CropChat benchmark has 242 tasks from 61 public repositories in 14 programming languages. Across 12 model-harness setups the best reaches 39.3% Pass@1, the share solved on the first try, and the harness alone shifts Pass@1 by up to 8.4 percentage points for the same model.