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,046 Open 1,614 Closed
1,046 Open 1,614 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

Non-reference traits 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
#1226 by RustanLeino was closed Nov 7, 2023
@RustanLeino
3 ❤️ 1
Standard Library kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#117 by overlogged was closed Feb 11, 2020
1 ❤️ 1
Revise presentation of grammar in RM kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials
#2806 by davidcok was closed Mar 8, 2023
@davidcok
1 ❤️ 1
Feature: Provide summary of all assumptions in a Dafny program difficulty: hard Issues that will take more than a week to fix kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
#2236 by atomb was closed Sep 27, 2022
@atomb @cpitclaudel
1 ❤️ 1
Standard library for Dafny kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#482 by davidcok was closed Sep 22, 2021
3 ❤️ 1
Measure verification time per "assertion" kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1597 by robin-aws was closed Jan 20, 2022 Verification Durability
@robin-aws
3 ❤️ 1
Resolver interprets name as a module instead of a type in type position kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
#1996 by mschlaipfer was closed Sep 21, 2022
1
@RustanLeino
21 ❤️ 1
Combined expect/assert kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#3410 by davidcok was closed Apr 22, 2023
1
10 ❤️ 1
Dafny 4.0 suggestion: opaque keyword 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
#2337 by MikaelMayer was closed Feb 8, 2023 Dafny 4.0
1
@RustanLeino
17 ❤️ 1
Fatal exception in parser (?)
#3 by plaidfinch was closed Jun 30, 2016
@qunyanm
feature request: naming function return values kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5 by Chris-Hawblitzel was closed Jan 20, 2017
@qunyanm
1
feature request: declaring constants kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#6 by Chris-Hawblitzel was closed Nov 30, 2016
@qunyanm
3
missing "ghost" keywords when printing expressions in methods
#8 by danmatichuk was closed Jul 12, 2016
@danmatichuk
Trigger loop introduced by the new fuel-based reveal
#9 by parno was closed Jul 16, 2016
@parno
opaque and literals
#11 by Chris-Hawblitzel was closed Sep 16, 2016
@parno
1
Dafny's occurs-check for type synonyms can be tricked
#12 by plaidfinch was closed Aug 5, 2016
@plaidfinch
Deep function causes Dafny Visual Studio extension to hang
#14 by jaylorch was closed Jul 26, 2016
@jaylorch
Compilation Error: generates duplicate local variable declarations
#15 by laurejt was closed Jul 26, 2016
@laurejt
Assertion failure in CompatibleDecreasesTypes with bv32 type
#26 by 0xabu was closed Oct 6, 2016
@qunyanm
function lemma in "ensures" doesn't work in 1.9.8 (worked in 1.9.7) 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)
#25 by xinhaoyuan was closed May 11, 2022
3
quantifiers over types that might be heap types difficulty: hard Issues that will take more than a week to fix 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) part: verifier Translation from Dafny to Boogie (translator)
#19 by Chris-Hawblitzel was closed Feb 23, 2023
1
@jtristan @RustanLeino
5
opaque leaked through consequence axiom
#20 by Chris-Hawblitzel was closed Sep 2, 2016
@parno
Dafny fails, but returns exit status of zero kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#21 by 0xabu was closed Sep 22, 2016
@qunyanm
Dafny VS extension crashes when including lengthy files
#24 by parno was closed Sep 2, 2016
@parno
Valid Lhs of a Method call with multiple out-parameters part: documentation Dafny's reference manual, tutorial, and other materials
#5660 by fabiomadge was closed Aug 2, 2024
1
1
ProTip! What’s not been updated in a month: updated:<2024-07-06.