Skip to content

Issues: dafny-lang/dafny

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
393 Open 781 Closed
393 Open 781 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Internal error when using improper trigger expression forall y: int {:trigger y} kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6201 opened Apr 22, 2025 by cdstanford
Internal Error - Call to Undeclared Procedure kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#6192 opened Apr 14, 2025 by nwad123
Model parsing error on Windows crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: counterexamples Counterexample generation
#6189 opened Apr 12, 2025 by croizier
2
Crash on undeclared LHS of :- crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#6184 opened Apr 7, 2025 by RustanLeino
Malformed Boogie in match inside forall kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#6183 opened Apr 7, 2025 by RustanLeino
1
New resolver is too restrictive when deciding on comparability of types incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#6181 opened Apr 6, 2025 by fabiomadge
1
Complex counterexample kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: counterexamples Counterexample generation
#6165 opened Mar 27, 2025 by m-carrasco
1
Dafny proves false using some complicated loop invariants during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6158 opened Mar 17, 2025 by anthowan
10
Java tries to use unboxed primitive types for type parameters in trait method overrides during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
#6147 opened Mar 10, 2025 by robin-aws
@VerifyOnly not working kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6146 opened Mar 10, 2025 by MikaelMayer
LSP error of type "Parse error"/"Invalid Request" is missing the "id" property kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6128 opened Feb 27, 2025 by robflop
Error reporting kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6126 opened Feb 26, 2025 by Osmansiddiquer
Cannot verify postcondition in lambda incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6117 opened Feb 19, 2025 by alexstaeding
Unable to verify function with parameters that are subset types only with '--type-system-refresh' kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
#6116 opened Feb 19, 2025 by alexstaeding
Proof for Unreachability requires assert false kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6114 opened Feb 18, 2025 by TomSMaier
f.requires forgotten for f defined with requires clause incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6110 opened Feb 17, 2025 by erniecohen
Compilation of raw backslash is failing in C# backend difficulty: good-first-issue Good first issues during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6109 opened Feb 17, 2025 by MikaelMayer
1
Revealed axiom doesn't make it to SMT solver kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6104 opened Feb 12, 2025 by RustanLeino
@keyboardDrummer
Noop && operation changes verification time kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator)
#6103 opened Feb 12, 2025 by keyboardDrummer
3
Verifier crash when dereferencing map constant/function kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6099 opened Feb 7, 2025 by erniecohen
1
Java backend: Unboxed bool return type in trait implementations kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6094 opened Feb 4, 2025 by eivindfjeldstad
Unsoundness of type verification caused by update syntax kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6089 opened Jan 30, 2025 by GenericMonkey
Vars in traits can't be part of extend reveals clauses and it crashes Dafny kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6080 opened Jan 24, 2025 by MikaelMayer
Using :| operator to create a set with a forall condition results in Boogie internal error during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done
#6071 opened Jan 23, 2025 by GenericMonkey
1
Definite-assignment in specification depends on implementation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#6064 opened Jan 22, 2025 by RustanLeino
6
ProTip! Follow long discussions with comments:>50.