on-prem 
Kill the tail, not the cores: profiling the verifier under RL-with-verifiers
As RL-with-verifiers scales, the Lean verifier is both the reward source and the throughput bottleneck — a CPU/scheduling problem almost nobody benchmarks on commodity, on-prem hardware. We profiled it: on an 8-core box, ~4.5% of proofs run away and eat most of the single-thread wall, and a tuned per-proof deadline beats adding cores. The honest-measurer story (including the claim we had to retract) is the point.
Your edge LLM can't tell time — and a 40-line memory can fix it (for some models)
A tiny adversarial benchmark shows small local LLMs confuse token-distance for elapsed wall-clock time. A zero-dependency continuous-time memory fixes it for sub-millisecond cost — but whether a model will even accept that fix turns out to be a model-dependent deployability property that capability leaderboards don’t measure.