Keystone — the certified decision engine

Ask a chatbot for a staff schedule and it hands you a fluent, often cheaper, INFEASIBLE plan — one that quietly staffs an ICU shift with an unqualified nurse. For any decision a business must stand behind, "plausible" isn't good enough — you need a plan you can prove. That's the problem Keystone owns. Keystone splits the decision into three separated roles, and the separation IS the product. PROPOSE: Gemma reads the messy natural-language problem — data tables plus plain-English rules and an objective — and emits a formal optimization model. DECIDE: OR-Tools CP-SAT solves it exactly, to a proof of optimality — or, when no plan exists, returns the minimal conflicting set of rules, the "why not." CERTIFY: an INDEPENDENT verifier re-checks every hard constraint from scratch with exact integer arithmetic and recomputes the objective; it never trusts the solver. The output is a machine-checkable Certificate and decision-pack. That same verifier exposes a raw-LLM baseline head-to-head — cheaper because it cheats, and not deployable. Use of AMD is real, not a checkbox. Keystone's core check — verify a schedule against every hard constraint — is a matrix multiply, so we run it as a batched float32 matmul on the MI300X's tensor cores (gpu_eval.py), scoring hundreds of thousands of candidates per second, bit-exact vs the CPU verifier. The MI300X notebook builds a 10,080-variable / 31,179-constraint roster and runs it through the same solve-then-certify path. Gemma proposes over one OpenAI-compatible path with three routes — vLLM-on-MI300X (the AMD-hosted prize route), Google AI Studio, or Fireworks. It's complete and runnable now: MOCK_MODE runs the whole pipeline offline with zero keys, yet the exact solver + verifier still run for real. Live demo, web console, REST + SSE API, Docker (+ ROCm image), 52 passing tests, MIT license. One core handles assignment, scheduling, allocation, selection, and matching — the moat a chatbot wrapper cannot cross.