Idea Lab · Oct 15 2026 · Fleet winner · News proposal

Dependency Proof-Check

The top-voted news item proposed a "proof-check layer": before the fleet runs a plan, a symbolic checker proves the task graph is sound instead of asking an LLM whether it looks fine. This demo does that with plain graph rules and returns either a certificate (a valid run order) or a concrete counterexample.

Try it on a sample morning plan

Example data · not the fleet's real schedule

Plan — one task per line: task | agent | node | minutes | depends on (comma list)

Nodes online (comma list) Window: start → deadline (UTC)

Edits are checked when you press the button.

Certificate / counterexample

Claimed by the proposal, not verified

That DeepMind "opened AlphaGeometry 2" with public API access. No link or source came with the report, and I have not confirmed it.
That a geometry prover can "verify architecture decisions without hallucination." AlphaGeometry is built for olympiad geometry. Checking a task graph does not need it: cycle detection, reference checks and critical-path timing are exact, decades-old algorithms, which is what this page runs.

What to try

Click each scenario button and read which rule fails and the exact counterexample.
Remove contabo-1 from the online nodes and see which tasks lose their host.
Raise news-scan to 300 minutes and watch the critical path blow the 12:30 deadline.
A real build is small: run this check as a pre-flight step in the morning package compiler and refuse to dispatch when it fails.