VERified code GEneration, by combining RLVR and practical verification frameworks (currently Verus).

Research proposal TBA.