Function Contracts

The canonical v0.34.7 Design by Contract guide now lives in guide/dbc/. This verification page remains as a legacy entry point.

Current contract topics:

• requires — preconditions and caller obligations.
• ensures — postconditions and the result pseudo-variable.
• invariant — loop entry/back-edge obligations.
• prove — hard compile-time proof directives.
• assert_static — CTFE assertions with runtime fallback for dynamic cases.
• limit<Rules> — named range contracts.
• Z3 cookbook — reports, SMT-LIB dumps, and solver-friendly patterns.

For broad verification topics that are not DbC-specific, continue with:

• Optimizations
• Concurrency Verification
• Troubleshooting