Search results

Proof block in spec fn to prove termination doesn't work due to bucket issue

Status: Open.

#1801 In verus-lang/verus;

· pratapsingh1729 opened on Jul 8, 2025

Verus panics on trigger

Status: Open.

#1795 In verus-lang/verus;

· Catoverflow opened on Jul 4, 2025

Comparing unequal consts in a precondition causes the function to always pass verification

Status: Open.

#1791 In verus-lang/verus;

· Furao opened on Jul 1, 2025

Support <code>#</code> in identifiers

Status: Open.

#1778 In verus-lang/verus;

· dschoepe opened on Jun 25, 2025

<code>--no-cheating</code> doesn't allow <code>Vec</code> indexing

Status: Open.

#1776 In verus-lang/verus;

· jaylorch opened on Jun 24, 2025

Regression: Commit a11f0f9 breaks cargo verus verify on log crate

Status: Open.

#1775 In verus-lang/verus;

· jasonbelt opened on Jun 23, 2025

empty enums / never type: unintuitive behavior

Status: Open.

#1764 In verus-lang/verus;

· tjhance opened on Jun 20, 2025

[lifetime generate] type annotations needed for generic fn value

Status: Open.

#1763 In verus-lang/verus;

· tjhance opened on Jun 20, 2025

<code>cargo verus build -- --no-lifetime</code> causes incorrect <code>cargo verus build</code>

Status: Open.

#1760 In verus-lang/verus;

· rsofaer opened on Jun 19, 2025

Flaky Proof in Anvil

Status: Open.

#1756 In verus-lang/verus;

· Catoverflow opened on Jun 19, 2025

Version the serialization format of the VIR bundle for a crate

Status: Open.

#1754 In verus-lang/verus;

· utaal opened on Jun 18, 2025

Panic on a non-Verus const inside a closure

Status: Open.

#1740 In verus-lang/verus;

· parno opened on Jun 12, 2025