Verification Flags

Tune timeouts, parallelism, integer semantics, and deterministic runs. Flags help keep proofs reproducible and fast enough to use.

Timeout Control

Set a wall-clock timeout for Viper/Silicon verification.

Run verification with multiple parallel worker threads.

Current verified code uses checked integer semantics. The --int-mode flag exists, but the Viper verification lane rejects bitvec and unchecked today.

Produce reproducible Viper artifacts with stable identifiers and consistent ordering.