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,021 Open 1,591 Closed
1,021 Open 1,591 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

[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5486 opened May 23, 2024 by aws-crypto-tools-ci-bot
36
Thoughts on a Dafny standard library? area: ffi The {:extern} attribute and otherwise interfacing with code in other languages kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
#1236 opened May 25, 2021 by parno
@wilcoxjay @parno
@RustanLeino @jaylorch
22
Add by blocks to function and method calls area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: language definition Relating to the Dafny language definition itself
#5192 opened Mar 13, 2024 by atomb
19
test fails: DafnyTests/TestAttribute.dfy platform: macOS macOS-specific issues status: needs-info Issue requires more information from poster
#1571 opened Nov 6, 2021 by hmijail
@MikaelMayer
19
measure-complexity non-deterministic? 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: tools Tools built on top of Dafny priority: next Will consider working on this after in progress work is done
#5126 opened Feb 24, 2024 by hmijail
1
@atomb
17
New Logo for Dafny part: documentation Dafny's reference manual, tutorial, and other materials priority: not yet Will reconsider working on this when we're looking for work
#4324 opened Jul 23, 2023 by booniepepper
17
Main methods should support a return value/process exit code kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny 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
#2699 opened Sep 6, 2022 by robin-aws
16
Cannot prove tautology with map, opaque function and transparent function. has-workaround: yes There is a known workaround incompleteness Things that Dafny should be able to prove, but can't part: boogie Happens after passing the program to Boogie part: verifier Translation from Dafny to Boogie (translator)
#2308 opened Jun 28, 2022 by MikaelMayer
1
16
CVC5 support? part: documentation Dafny's reference manual, tutorial, and other materials
#4100 opened May 29, 2023 by hmijail
@atomb
15
Incorrect printing of generically-typed strings in Go (a.k.a. should string != seq<char>?) breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends
#2582 opened Aug 11, 2022 by robin-aws
@robin-aws
15
Include subtypes in case patterns 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
#1715 opened Jan 14, 2022 by RustanLeino
14
Termination of dynamic dispatch kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#1588 opened Nov 13, 2021 by RustanLeino
14
Unsound verification with /proverOpt:O:smt.arith.solver=6 area: nonlinear arithmetic Support for reasoning about nonlinear arithmetic 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: pre-2009 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) priority: not yet Will reconsider working on this when we're looking for work
#4053 opened May 21, 2023 by muchang
@atomb
13
sequence comprehensions are ugly 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
#1332 opened Jul 29, 2021 by jonhnet
12
Flaky CI Test: LanguageServer.IntegrationTest.ProjectFiles.CompetingProjectFilesTest.ProjectFileDoesNotOwnAllSourceFilesItUses kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5420 opened May 10, 2024 by MikaelMayer
@keyboardDrummer
11
Unable to reason about types that extends a non-ref trait kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#4973 opened Jan 10, 2024 by txiang61
11
Unintuitive error location for errors on explicitly included dependency files area: error-reporting Clarity of the error reporting
#4977 opened Jan 11, 2024 by Rekkonnect
10
Potential Unsoundness in Prelude.bpl 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: pre-2009 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) priority: not yet Will reconsider working on this when we're looking for work
#4400 opened Aug 8, 2023 by yizhou7
@atomb @jtristan
10
No verification error when "reads this" is missing kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#3911 opened Apr 27, 2023 by benreynwar
10
Can we warn about curly braces in mistyped expression-level ifs? area: error-reporting Clarity of the error reporting kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2899 opened Oct 17, 2022 by cpitclaudel
10
Constant fields depending on non-initialized fields should not be usable in first-phase construction 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: pre-2012 part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#2727 opened Sep 12, 2022 by RustanLeino
1
@MikaelMayer
10
Dafny 4 Suggestion: Adaptors to fix usability of update with failure misc: language proposals Proposals for change to the language that go beyon simple enhancement requests
#2436 opened Jul 18, 2022 by davidcok
@davidcok
10
Assert failing in strange way kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny misc: brittleness When Dafny sometimes proves something, and sometimes doesn't part: verifier Translation from Dafny to Boogie (translator)
#1570 opened Nov 6, 2021 by hmijail
@robin-aws
10
Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5488 opened May 24, 2024 by keyboardDrummer
@robin-aws
9
Verification Regressions with Dafny 4.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#3758 opened Mar 20, 2023 by DavePearce
9
ProTip! Adding no:label will show everything without a label.