Design by Contract

The canonical v0.34.7 Design by Contract guide now lives in guide/dbc/.

Use that cookbook for current behavior of:

• requires
• ensures
• invariant
• prove
• assert_static
• limit<Rules>
• failsafe workflow
• Z3 debugging

This page remains as a compatibility entry point from the functions section.