assume #

Caution

Since the assume statement is unchecked, it can easily be used to subvert Verus's guarantees. In particular, successful "verification" by Verus provides no guarantees on the program if it includes any assume statements, unless those assume statements could in principle be replaced by a successful assert statement.

The assume statement is most useful during intermediate stages of development, e.g., within an assert/assume-driven proof-development process.