Search results

Unresolved identifiers when refining anonymous constructors

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6429 In dafny-lang/dafny;

· manuelmontenegro opened on Feb 4, 2026

Verification time slowdown after commit 281922d

Status: Open.

#6428 In dafny-lang/dafny;

· m-carrasco opened on Feb 1, 2026

Verification time slowdown after commit c9cffc3

Status: Open.

#6427 In dafny-lang/dafny;

· m-carrasco opened on Feb 1, 2026

Dafny uses incorrect accessor names for Java interfaces

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6425 In dafny-lang/dafny;

· fcseidl opened on Jan 29, 2026

Verification time slowdown after commit 2cc052c

Status: Open.

#6424 In dafny-lang/dafny;

· m-carrasco opened on Jan 25, 2026

Opaque blocks with nested functions in ensures clause

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6423 In dafny-lang/dafny;

· clid opened on Jan 15, 2026

Compilation to JS gets "Cannot find module 'bignumber.js'"

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6421 In dafny-lang/dafny;

· yaitskov opened on Jan 6, 2026

Verification incompleteness with bit vectors

incompletenessThings that Dafny should be able to prove, but can'tThings that Dafny should be able to prove, but can't

Status: Open.

#6420 In dafny-lang/dafny;

· MikaelMayer opened on Dec 30, 2025

Missing method-reads check in array initializer

difficulty: good-first-issueGood first issuesGood first issues

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

part: resolverResolution and typecheckingResolution and typechecking

Status: Open.

#6410 In dafny-lang/dafny;

· RustanLeino opened on Dec 4, 2025

Make the Translation keep code comments

kind: enhancementEnhancements, feature requests, etc. These are NOT bugs, but ways we can improve DafnyEnhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Status: Open.

#6409 In dafny-lang/dafny;

· ben-GDV opened on Dec 4, 2025

map with (literal) set as key treats set element order as significant

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6408 In dafny-lang/dafny;

· geert56 opened on Dec 3, 2025

<code>ensures false</code> conflicting behavior with and without <code>match</code>

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6405 In dafny-lang/dafny;

· JohnEdwardJennings opened on Dec 1, 2025