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,033 Open 1,599 Closed
1,033 Open 1,599 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

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
#1868 opened Feb 28, 2022 by atomb
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)
#1775 opened Feb 1, 2022 by robin-aws
@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
#1770 opened Jan 28, 2022 by robin-aws
@robin-aws
6
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
#1259 opened Jun 22, 2021 by robin-aws
6
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
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
random seed vs verification coverage report? part: documentation Dafny's reference manual, tutorial, and other materials
#5177 opened Mar 12, 2024 by hmijail
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
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
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
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
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
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
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
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
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
Enable configuring the Dafny version in the Dafny project file kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: CLI interacting with Dafny on the command line status: needs-approval Issue that needs approval from Dafny team members before moving to designed
#3848 opened Apr 5, 2023 by keyboardDrummer
5
Improve assertion failure wording kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3216 opened Dec 18, 2022 by Timmmm
1
5
Review/edit README page part: documentation Dafny's reference manual, tutorial, and other materials
#2632 opened Aug 23, 2022 by davidcok
@davidcok
5
Default to nameonly Dafny V4 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
#2318 opened Jun 29, 2022 by seebees
5
Iterating over sets in compiled code is slow area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#2062 opened Apr 23, 2022 by robin-aws
5
Feature request: verify resolved methods even if other methods can't be resolved kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking part: verifier Translation from Dafny to Boogie (translator)
#1784 opened Feb 3, 2022 by cpitclaudel
5
Timeouts and caching: should we set timeouts per assertion instead of per method? area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator) part: z3 Issue is in Z3
#1772 opened Jan 31, 2022 by cpitclaudel
5
Design Proposal: Support for enumeration part: language definition Relating to the Dafny language definition itself
#1753 opened Jan 21, 2022 by robin-aws
@robin-aws
5
Discussion: Versioning of the custom LSP API part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo)
#1562 opened Nov 5, 2021 by camrein
@camrein
5
ProTip! Add no:assignee to see everything that’s not assigned.