Search results

A bug in the interpreter

Status: Open.

#2110 In verus-lang/verus;

· SSSPigeon opened on Jan 22, 2026

audit uses of env_var

Status: Open.

#2106 In verus-lang/verus;

· tjhance opened on Jan 21, 2026

verusdoc: cannot display <code>ensures</code> and <code>requires</code>for <code>verus_spec</code>

Status: Open.

#2082 In verus-lang/verus;

· Marsman1996 opened on Jan 18, 2026

Trait extension plus Verus attributes produces spurious warnings

Status: Open.

#2080 In verus-lang/verus;

· parno opened on Jan 16, 2026

Panic when proof_fn (proof closures) are bound without <code>tracked</code>

Status: Open.

#2078 In verus-lang/verus;

· y1ca1 opened on Jan 12, 2026

[cargo-verus] refactor to allow end-to-end testing without running a child process

Status: Open.

#2068 In verus-lang/verus;

· mkovaxx opened on Jan 8, 2026

Document cfg verus_keep_ghost and perhaps add it to cargo-verus new template

Status: Open.

#2063 In verus-lang/verus;

· sssxks opened on Dec 31, 2025

bad error msg for proof block in proof fn

Status: Open.

#2061 In verus-lang/verus;

· tjhance opened on Dec 30, 2025

Panic when invoking a function on a trait generated by external_trait_extension

Status: Open.

#2047 In verus-lang/verus;

· parno opened on Dec 19, 2025

[Feature Request] Better Isolation for Match

Status: Open.

#2038 In verus-lang/verus;

· Catoverflow opened on Dec 16, 2025

decrease_when allows non-terminating spec function

Status: Open.

#2036 In verus-lang/verus;

· WeituoDAI opened on Dec 15, 2025

Integer casting for type implements builtin::Integer does not work properly when used with verifier::inline

Status: Open.

Bug

#2031 In verus-lang/verus;

· ziqiaozhou opened on Dec 8, 2025