Can robots learn skills that actually satisfy safety rules?

Robot skills built from large language models work in practice but lack guarantees they'll behave safely in new situations. VASO combines formal verification with skill evolution: a model checker finds safety violations in LLM-generated robot behaviors, then converts counterexamples into text-based feedback to refine the skill contract itself—not the model weights. On real robots (wheeled and quadcopter), this reaches 97% formal compliance with minimal samples, outperforming execution feedback and prompt tuning alone.