Search results

Note on trigger-mode option is incorrect

Status: Open.

#1862 In verus-lang/verus;

· rod-chapman opened on Aug 12, 2025

panic on duplicate specification for a method that is also <code>derive</code>d

Status: Open.

#1861 In verus-lang/verus;

· gewitternacht opened on Aug 12, 2025

Use of named constants in contracts with bit_vector solver

Status: Open.

#1858 In verus-lang/verus;

· rod-chapman opened on Aug 8, 2025

Support for mixed sign and size in integer type conversions

Status: Open.

#1854 In verus-lang/verus;

· rod-chapman opened on Aug 6, 2025

Documenting how to build with Singular

Status: Open.

#1852 In verus-lang/verus;

· rod-chapman opened on Aug 4, 2025

assertions of call_requires.

Status: Open.

#1848 In verus-lang/verus;

· RorroArt opened on Jul 31, 2025

Verus panics on "ill-typed AIR code" when mutual recursive <code>decreases</code> metrics have different types

Status: Open.

#1845 In verus-lang/verus;

· pratapsingh1729 opened on Jul 28, 2025

const &amp;str now requires explicit lifetime

Status: Open.

#1838 In verus-lang/verus;

· rsofaer opened on Jul 23, 2025

<code>HashMap::clone</code> allows to prove false facts with a non-standard <code>Clone</code> implementation

Status: Open.

#1835 In verus-lang/verus;

· gewitternacht opened on Jul 22, 2025

invalid AIR from allow_in_spec

Status: Open.

#1834 In verus-lang/verus;

· tjhance opened on Jul 22, 2025

Fails to prove termination when recursive calls are placed inside a loop

Status: Open.

#1832 In verus-lang/verus;

· rikosellic opened on Jul 21, 2025

Verus allows using <code>matches</code> in executable code

Status: Open.

#1830 In verus-lang/verus;

· dschoepe opened on Jul 20, 2025