Begin a formal proof of the LVT-based 1W/1R wrapper