verify: document some 'assume' pitfalls