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,113 Open 1,667 Closed
1,113 Open 1,667 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

Parsing error for set comparison within array initialisation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: not yet Will reconsider working on this when we're looking for work
#5698 opened Aug 14, 2024 by kbuaaaaaa
2
Measure verification performance of Dafny integration test suite kind: language development speed Slows down development of Dafny the language, flaky tests misc: brittleness When Dafny sometimes proves something, and sometimes doesn't
#5693 opened Aug 13, 2024 by keyboardDrummer
Add a code action that automatically adds hide and reveal statements to a proof. 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
#5692 opened Aug 13, 2024 by keyboardDrummer
Allow hiding ensures clauses 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 priority: not yet Will reconsider working on this when we're looking for work
#5691 opened Aug 13, 2024 by keyboardDrummer
Improvement suggestions for the Dafny AST (AST.dfy) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny priority: not yet Will reconsider working on this when we're looking for work
#5690 opened Aug 13, 2024 by dnezam
10 tasks
3
Isolate all implicit assertions 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
#5689 opened Aug 13, 2024 by keyboardDrummer
Allow providing isolated proofs for the preconditions of function calls and operators 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
#5688 opened Aug 13, 2024 by keyboardDrummer
@keyboardDrummer
Opaque block 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
#5687 opened Aug 13, 2024 by keyboardDrummer
Allow hiding subset types 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
#5686 opened Aug 13, 2024 by keyboardDrummer
--outer-module not tracked for empty parent modules
#5683 opened Aug 12, 2024 by robin-aws
Dafny server does not correctly show errors for postconditions of function 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)
#5678 opened Aug 9, 2024 by keyboardDrummer
@keyboardDrummer
dafny run crashes on print @"\"; kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5677 opened Aug 9, 2024 by dnezam
1
Support for Rust tests kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5666 opened Aug 5, 2024 by MikaelMayer
Verifier crash on match within assert by within function
#5671 opened Aug 5, 2024 by erniecohen
1
Dafny-to-Rust: SelectFn should produce a tree instead of a raw string
#5664 opened Aug 2, 2024 by MikaelMayer
Bad code generated for edge-case when using generate-tests 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: test generation Relates to the dafny generate-tests command
#5658 opened Jul 31, 2024 by keyboardDrummer
Fragility issue when inherited trait function used in inherited contract kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5652 opened Jul 29, 2024 by erniecohen
1
Some type errors lack error messages with --type-system-refresh kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5646 opened Jul 23, 2024 by dschoepe
@RustanLeino
Rust backend needs an option similar to --go-module-name or --python-module-name
#5641 opened Jul 21, 2024 by robin-aws
4
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
#5640 opened Jul 21, 2024 by aws-crypto-tools-ci-bot
119
Better path error reporting 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: verifier Translation from Dafny to Boogie (translator)
#5628 opened Jul 16, 2024 by keyboardDrummer
Flaky test: ChangedImportAffectsExport kind: language development speed Slows down development of Dafny the language, flaky tests
#5619 opened Jul 11, 2024 by MikaelMayer
function transparency vs isolate-assertions vs split_here misc: question Questions about Dafny's implementation. For beginner questions use "discussions" or StackOverflow
#5618 opened Jul 11, 2024 by hmijail
4
transparent function == verified multiple times? part: documentation Dafny's reference manual, tutorial, and other materials
#5617 opened Jul 11, 2024 by hmijail
1
Busy z3 process leaked kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5616 opened Jul 11, 2024 by hmijail
1
ProTip! Exclude everything labeled bug with -label:bug.