Provably optimal lot dispatch
Decide which lot runs next on which tool as queues, set-ups and re-entrant flows change. Each policy comes with bounds on deadlines and waiting times, and is checked against them before it is used on the floor. On the Mini-Fab benchmark, we proved in Lean a lower bound over every possible policy, and found a policy that meets it exactly.