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
1,093 Open 1,648 Closed
1,093 Open 1,648 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

Incomplete regression for Dafny 4.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3869 opened Apr 14, 2023 by muchang
5
Dafny does not have a binary release for Linux arm64 kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: z3 Issue is in Z3
#3972 opened May 8, 2023 by tchajed
5
Release process enhancement: check downstream nightly builds before releasing kind: language development speed Slows down development of Dafny the language, flaky tests
#4222 opened Jun 28, 2023 by robin-aws
5
Dafny crash when there is "e in S" set membership syntax and an export set crash Dafny crashes on this input, or generates malformed code that can not be executed 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 part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done status: needs-info Issue requires more information from poster
#4334 opened Jul 25, 2023 by sjjs7
1
5
this is not fresh and fresh in well-formedness 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 introduced: v4.1.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
#4700 opened Oct 20, 2023 by MikaelMayer
1
5
Can't Prove Subset Constraints without Assert during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program 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 kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself priority: not yet Will reconsider working on this when we're looking for work
#4725 opened Oct 27, 2023 by whonore
5
Incompleteness issue in the configuration /arith:3 to 8 when using "as" in a division. kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5004 opened Jan 23, 2024 by muchang
5
IDE does not provide feedback if the solver can not be started 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 part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) priority: next Will consider working on this after in progress work is done
#5131 opened Feb 27, 2024 by Timmmm
@keyboardDrummer
5
Type mismatch allowed in ensures clause with type parameters and datatypes during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: next Will consider working on this after in progress work is done
#5144 opened Mar 4, 2024 by atomb
5
Single expression for combined is and as kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5165 opened Mar 8, 2024 by robin-aws
5
random seed vs verification coverage report? part: documentation Dafny's reference manual, tutorial, and other materials
#5177 opened Mar 12, 2024 by hmijail
5
Warn about potential brittleness due to use of difficult constructs kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5253 opened Mar 26, 2024 by atomb
@atomb
5
Unstable CLI test git-issues/git-issue-697j.dfy, related to Rust backend kind: language development speed Slows down development of Dafny the language, flaky tests part: ci Issue is with Dafny's CI infrastructure priority: not yet Will reconsider working on this when we're looking for work
#5537 opened Jun 6, 2024 by keyboardDrummer
5
C++ support for unconstrained ints kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c++ Dafny's C++ transpiler and its runtime misc: update Updates to a Dafny dependency part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#1259 opened Jun 22, 2021 by robin-aws
6
Track which compilers support which Dafny features kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work
#1770 opened Jan 28, 2022 by robin-aws
@robin-aws
6
(Idea) Implement built-in Dafny types in Dafny source code kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant) priority: not yet Will reconsider working on this when we're looking for work
#1775 opened Feb 1, 2022 by robin-aws
@robin-aws
6
Exponents not allowed in real literals kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself priority: not yet Will reconsider working on this when we're looking for work
#1868 opened Feb 28, 2022 by atomb
6
Incorrect axiom for .requires on lambda term during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't part: verifier Translation from Dafny to Boogie (translator) priority: not yet Will reconsider working on this when we're looking for work status: designed Issues that have a complete story on how to implement this feature and why we want it
#2137 opened May 12, 2022 by atomb
6
Dafny 4.0 suggestion: Get rids of returns keyword to unify function, predicate and methods breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2342 opened Jun 30, 2022 by MikaelMayer
6
Dafny 4.0 suggestion: get modern assignment operators breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2345 opened Jun 30, 2022 by MikaelMayer
6
Implement lazy sequence concatenation in remaining backends kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c++ Dafny's C++ transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime lang: python Dafny's Python transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#2390 opened Jul 11, 2022 by robin-aws
@robin-aws
6
Feat: Inner methods / closures modifying the heap kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3392 opened Jan 23, 2023 by MikaelMayer
6
Cannot prove extremely simple equality already stated. has-workaround: yes There is a known workaround 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
#3863 opened Apr 12, 2023 by MikaelMayer
6
Comma-separated expressions using <, > operators parsed as type area: error-reporting Clarity of the error reporting part: parser First phase of Dafny's pipeline
#3932 opened May 1, 2023 by alex-usher
6
Organization of CI workflow impedes restarting individual jobs kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4102 opened May 30, 2023 by davidcok
@atomb
6
ProTip! Exclude everything labeled bug with -label:bug.