nickh007/specforge-leaderboard

Can your solver demonstrate what it claims?

Paste a submission; it is scored with every counterexample replayed against the real model. A claim without a trace that replays earns nothing.

Tasks are generated deterministically from the count, seed and difficulty. Changing the seed changes the task set. The JSON export contains solver inputs, omitting verdicts, counterexample lengths and answer-bearing builder metadata. Ground truth and generation code remain public: this is a public scoring demo, not a blind evaluation. Everything runs in your browser under Pyodide; nothing is uploaded anywhere.

Press "Run the fabricated-trace oracle." It has perfect labels and invented evidence, and it scores exactly what guessing scores. That gap — between accuracy and accuracy_ignoring_replay — is the whole measurement.

• —Generator: nickharris808/specforge
• —Dataset: nickh007/specforge
• —Checker: nickharris808/minicheck

Honest scope. A score measures how well a solver finds and demonstrates safety violations in synthetic finite state machines at a given size. It says nothing about real-world protocol implementations, and nothing comparable across seeds unless you report which one you used. Nothing here asserts anything about any named third-party protocol or product.