Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/dafny-lang/dafny

Dafny is a verification-aware programming language

https://github.com/dafny-lang/dafny

Science Score: 36.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ✓
    Committers with academic emails
    14 of 121 committers (11.6%) from academic institutions
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (10.8%) to scientific vocabulary

Keywords

programming-language verification

Keywords from Contributors

agents archived transformers interaction observability sequences distributed parallel projection cryptocurrencies
Last synced: 5 months ago · JSON representation

Repository

Dafny is a verification-aware programming language

Basic Info
  • Host: GitHub
  • Owner: dafny-lang
  • License: other
  • Language: C#
  • Default Branch: master
  • Homepage: https://dafny.org
  • Size: 313 MB
Statistics
  • Stars: 3,149
  • Watchers: 81
  • Forks: 282
  • Open Issues: 1,316
  • Releases: 52
Topics
programming-language verification
Created almost 10 years ago · Last pushed 6 months ago
Metadata Files
Readme Contributing License Code of conduct Security

README.md

Dafny

Build and Test Gitter

Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.

vs-code-dafny-2 0 0-demo

Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing.

Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures.

Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.

Dafny

This github site contains these materials:

Documentation about the Dafny language and tools is located here. A reference manual is available both online and as pdf. (A LaTeX version can be produced if needed.)

Community

Feel free to report issues here on GitHub or to ask for questions on our :speech_balloon: Zulip channel.

Try Dafny

The easiest way to try out Dafny is to install Dafny on your own machine in Visual Studio Code and follow along with the Dafny tutorial. You can also download and install the Dafny CLI if you prefer to work from the command line.

Read more

Here are some ways to get started with Dafny:

The language itself draws pieces of influence from:

  • Euclid (from the mindset of a designing a language whose programs are to be verified),
  • Eiffel (like the built-in contract features),
  • CLU (like its iterators, and inspiration for the out-parameter syntax),
  • Java, C#, and Scala (like the classes and traits, and syntax for functions),
  • ML (like the module system, and its functions and inductive datatypes), and
  • Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).

External contributions

Contributors

Information and instructions for potential contributors are provided here.

License

Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory Source/Dafny/Coco contains third party material; see Source/DafnyCore/Coco/LICENSE.txt for more details.

Committers

Last synced: 9 months ago

All Time
  • Total Commits: 6,265
  • Total Committers: 121
  • Avg Commits per committer: 51.777
  • Development Distribution Score (DDS): 0.807
Past Year
  • Commits: 328
  • Committers: 22
  • Avg Commits per committer: 14.909
  • Development Distribution Score (DDS): 0.68
Top Committers
Name Email Commits
Rustan Leino l****o@m****m 1,210
Rustan Leino l****o@a****m 811
Remy Willems r****s@a****m 572
David Cok d****k@g****m 418
Mikaël Mayer M****r 349
Clément Pit--Claudel c****l@l****m 257
Robin Salkeld s****r@a****m 236
Valentin Wuestholz w****z@g****m 212
qunyanm q****m@h****m 197
Fabio Madge f****e@a****m 159
Aaron Tomb a****b@a****m 142
Prathamesh Bang p****g@a****m 131
Luke Maurer l****r@g****m 129
davidcok d****k@a****m 121
Daniel Matichuk d****k@g****m 105
Jack Sturtevant j****e@a****m 105
Jason Koenig j****g@s****u 88
Bryan Parno p****o@m****m 79
Aleksandar Milicevic a****s@c****u 60
Markus Schaden m****n@g****m 57
Nadia Polikarpova n****a@g****m 47
James Wilcox j****2@c****u 47
Alex Chew a****w 47
davidcok d****k@g****m 47
Aleksandr Fedchin s****n@g****m 39
dependabot[bot] 4****] 38
Samuel Gruetter k****t@a****m 35
Bryan Parno p****o@c****u 29
Shadaj Laddad s****j 28
Dan Rosen d****r@c****e 26
and 91 more...
Committer Domains (Top 20 + Academic)
amazon.com: 18 microsoft.com: 10 csail.mit.edu: 2 cs.washington.edu: 2 inf.ethz.ch: 2 github.com: 2 galois.com: 1 stanford.edu: 1 cmu.edu: 1 chalmers.se: 1 uta.fi: 1 uwaterloo.ca: 1 alum.mit.edu: 1 cs.cmu.edu: 1 in.tum.de: 1 cs.utexas.edu: 1 raphael.dasgupta.ch: 1 nuim.ie: 1 afd-think.home: 1 adacore.com: 1

Issues and Pull Requests

Last synced: 6 months ago

All Time
  • Total issues: 1,203
  • Total pull requests: 1,847
  • Average time to close issues: 7 months
  • Average time to close pull requests: 15 days
  • Total issue authors: 146
  • Total pull request authors: 52
  • Average comments per issue: 1.47
  • Average comments per pull request: 0.53
  • Merged pull requests: 1,361
  • Bot issues: 0
  • Bot pull requests: 44
Past Year
  • Issues: 224
  • Pull requests: 637
  • Average time to close issues: 7 days
  • Average time to close pull requests: 6 days
  • Issue authors: 58
  • Pull request authors: 26
  • Average comments per issue: 0.74
  • Average comments per pull request: 0.39
  • Merged pull requests: 447
  • Bot issues: 0
  • Bot pull requests: 12
View more stats
Top Authors
Issue Authors
  • MikaelMayer (151)
  • robin-aws (144)
  • keyboardDrummer (140)
  • RustanLeino (90)
  • cpitclaudel (48)
  • erniecohen (40)
  • atomb (36)
  • dafny-lang-bot (35)
  • davidcok (34)
  • aws-crypto-tools-ci-bot (31)
  • hmijail (25)
  • fabiomadge (22)
  • seebees (21)
  • ajewellamz (19)
  • sorawee (15)
Pull Request Authors
  • keyboardDrummer (573)
  • MikaelMayer (300)
  • RustanLeino (168)
  • atomb (152)
  • robin-aws (115)
  • fabiomadge (112)
  • alex-chew (54)
  • dependabot[bot] (44)
  • davidcok (41)
  • shadaj (30)
  • Dargones (29)
  • jtristan (26)
  • olivier-aws (25)
  • stefan-aws (19)
  • ssomayyajula (19)
Top Labels
Issue Labels
kind: bug (653) kind: enhancement (235) priority: not yet (122) part: verifier (99) part: resolver (85) during 2: compilation of correct program (81) part: code-generation (72) kind: language development speed (65) crash (65) priority: next (62) status: fixed (61) part: documentation (53) lang: java (42) part: language server (39) during 1: program development (37) during 3: execution of incorrect program (29) area: error-reporting (29) has-workaround: yes (22) part: standard libraries (22) misc: cleanup (22) incompleteness (21) lang: c# (19) release-blocker (19) misc: brittleness (19) part: language definition (16) lang: python (16) invalid translated code (16) makes-mikael-grateful (15) testing-method: uniform-backend-testing (14) area: performance (14)
Pull Request Labels
run-deep-tests (102) dependencies (44) github_actions (29) run-integration-tests (23) ruby (13) part: counterexamples (4) severity: release-blocker (3) makes-mikael-grateful (2) .NET (2) skip-deep-tests (1) need-check-proof-variability (1) breaking-change (1) kind: enhancement (1) part: documentation (1) priority: not yet (1) kind: bug (1)

Packages

  • Total packages: 3
  • Total downloads:
    • pypi 49,723 last-month
    • homebrew 91 last-month
  • Total dependent packages: 0
    (may contain duplicates)
  • Total dependent repositories: 1
    (may contain duplicates)
  • Total versions: 94
  • Total maintainers: 1
proxy.golang.org: github.com/dafny-lang/dafny
  • Versions: 55
  • Dependent Packages: 0
  • Dependent Repositories: 0
Rankings
Stargazers count: 0.9%
Forks count: 1.2%
Average: 4.6%
Dependent packages count: 7.0%
Dependent repos count: 9.3%
Last synced: 6 months ago
formulae.brew.sh: dafny

Verification-aware programming language

  • Versions: 28
  • Dependent Packages: 0
  • Dependent Repositories: 1
  • Downloads: 91 Last month
Rankings
Stargazers count: 9.9%
Forks count: 10.6%
Dependent packages count: 18.4%
Average: 19.8%
Dependent repos count: 29.3%
Downloads: 30.6%
Last synced: 6 months ago
pypi.org: dafnyruntimepython

Dafny runtime for Python

  • Versions: 11
  • Dependent Packages: 0
  • Dependent Repositories: 0
  • Downloads: 49,723 Last month
Rankings
Dependent packages count: 10.0%
Average: 37.9%
Dependent repos count: 65.8%
Maintainers (1)
dafny
Last synced: 6 months ago

Dependencies

.github/workflows/check-deep-tests-reusable.yml actions
  • actions/checkout v3 composite
  • actions/github-script v6 composite
.github/workflows/doc-tests.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
.github/workflows/integration-tests-reusable.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
  • actions/setup-java v3 composite
  • actions/setup-node v3 composite
  • actions/setup-python v4 composite
  • actions/upload-artifact v3 composite
.github/workflows/msbuild.yml actions
  • actions/checkout v3 composite
  • actions/download-artifact v3 composite
  • actions/setup-dotnet v3 composite
  • actions/upload-artifact v3 composite
  • irongut/CodeCoverageSummary v1.3.0 composite
.github/workflows/publish-release-reusable.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
  • actions/setup-java v3 composite
  • actions/setup-node v3 composite
  • actions/setup-python v4 composite
  • actions/upload-artifact v3 composite
  • softprops/action-gh-release v1 composite
.github/workflows/publish-release.yml actions
  • battila7/get-version-action v2 composite
.github/workflows/refman.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
  • actions/upload-artifact v3 composite
.github/workflows/release-brew.yml actions
  • actions/setup-python v4 composite
.github/workflows/release-downloads-nuget.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
  • actions/setup-java v3 composite
  • pozetroninc/github-action-get-latest-release v0.5.0 composite
.github/workflows/release-downloads.yml actions
  • actions/setup-java v3 composite
  • dsaltares/fetch-gh-release-asset master composite
.github/workflows/runtime-tests.yml actions
  • actions/checkout v3 composite
  • actions/setup-java v3 composite
.github/workflows/test-report.yml actions
  • actions/checkout v3 composite
  • dorny/test-reporter v1 composite
.github/workflows/xunit-tests-reusable.yml actions
  • actions/checkout v3 composite
  • actions/setup-dotnet v3 composite
  • actions/upload-artifact v3 composite
Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock cargo
  • autocfg 1.1.0
  • either 1.9.0
  • itertools 0.11.0
  • num 0.4.1
  • num-bigint 0.4.3
  • num-complex 0.4.4
  • num-integer 0.1.45
  • num-iter 0.1.43
  • num-rational 0.4.1
  • num-traits 0.2.16
  • once_cell 1.18.0
  • paste 1.0.14
Source/DafnyRuntime/DafnyRuntimeRust/Cargo.toml cargo
Source/DafnyRuntime/DafnyRuntimeJava/build.gradle maven
  • org.junit.jupiter:junit-jupiter-engine 5.5.2 testImplementation
Test/benchmarks/sequence-race/java/build.gradle.kts maven
  • org.dafny:DafnyRuntime 4.2.0 implementation
  • org.junit.jupiter:junit-jupiter-api 5.9.2 testImplementation
  • org.junit.jupiter:junit-jupiter-engine * testRuntimeOnly
Source/AutoExtern/AutoExtern.csproj nuget
  • Microsoft.Build 17.0.0
  • Microsoft.Build.Framework 17.0.0
  • Microsoft.Build.Locator 1.4.1
  • Microsoft.Build.Tasks.Core 17.0.0
  • Microsoft.Build.Utilities.Core 17.0.0
  • Microsoft.CodeAnalysis 4.0.1
  • Microsoft.CodeAnalysis.CSharp 4.0.1
  • Microsoft.CodeAnalysis.CSharp.Workspaces 4.0.1
  • Microsoft.CodeAnalysis.Workspaces.MSBuild 4.0.1
  • System.CommandLine 2.0.0-beta4.22272.1
Source/AutoExtern.Test/AutoExtern.Test.csproj nuget
  • Microsoft.NET.Test.Sdk 16.11.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/AutoExtern.Test/Minimal/Library.csproj nuget
Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj nuget
Source/AutoExtern.Test/Tutorial/Library/Library.csproj nuget
Source/Dafny/Dafny.csproj nuget
Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj nuget
Source/DafnyCore/DafnyCore.csproj nuget
  • Boogie.ExecutionEngine 3.0.4
  • JetBrains.Annotations 2021.1.0
  • Microsoft.CodeAnalysis.CSharp 3.7.0
  • Microsoft.Extensions.FileSystemGlobbing 5.0.0
  • Microsoft.Extensions.Logging.Abstractions 5.0.0
  • System.Collections.Immutable 1.7.0
  • System.CommandLine 2.0.0-beta4.22272.1
  • System.Runtime.Numerics 4.3.0
  • Tomlyn 0.16.2
Source/DafnyCore.Test/DafnyCore.Test.csproj nuget
  • Microsoft.NET.Test.Sdk 17.1.0
  • coverlet.collector 3.2.0
  • xunit 2.4.1
  • xunit.runner.visualstudio 2.4.3
Source/DafnyDriver/DafnyDriver.csproj nuget
  • Microsoft.TestPlatform.Extensions.TrxLogger 17.0.0
  • Microsoft.TestPlatform.TestHost 16.11.0
  • Newtonsoft.Json 13.0.1
  • System.Collections 4.3.0
  • System.Diagnostics.Debug 4.3.0
  • System.IO.FileSystem.Primitives 4.3.0
  • System.Runtime.Handles 4.3.0
  • System.Runtime.InteropServices 4.3.0
  • System.Security.Principal.Windows 4.6.0
  • System.Text.Encoding.Extensions 4.3.0
  • System.Threading 4.3.0
Source/DafnyDriver.Test/DafnyDriver.Test.csproj nuget
  • Microsoft.NET.Test.Sdk 17.1.0
  • OmniSharp.Extensions.JsonRpc 0.19.5
  • OmniSharp.Extensions.LanguageProtocol 0.19.5
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.extensibility.core 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/DafnyLanguageServer/DafnyLanguageServer.csproj nuget
  • Microsoft.Extensions.Configuration.CommandLine 5.0.0
  • Microsoft.Extensions.Configuration.Json 5.0.0
  • Microsoft.Extensions.Logging 5.0.0
  • Newtonsoft.Json 13.0.1
  • OmniSharp.Extensions.LanguageServer 0.19.5
  • RangeTree 3.0.1
  • Serilog 2.10.0
  • Serilog.Extensions.Logging 3.0.1
  • Serilog.Settings.Configuration 3.1.0
  • Serilog.Sinks.Debug 2.0.0
  • Serilog.Sinks.File 5.0.0
  • System.Collections 4.3.0
  • System.Diagnostics.Debug 4.3.0
  • System.IO.FileSystem.Primitives 4.3.0
Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj nuget
  • DiffPlex 1.7.0
  • Microsoft.CodeAnalysis.CSharp 3.7.0
  • Microsoft.Extensions.Logging.Console 5.0.0
  • Microsoft.NET.Test.Sdk 17.1.0
  • Moq 4.16.1
  • OmniSharp.Extensions.LanguageProtocol.Testing 0.19.5
  • Serilog.Sinks.InMemory 0.11.0
  • Xunit.AssertMessages 2.4.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.extensibility.core 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/DafnyPipeline/DafnyPipeline.csproj nuget
Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj nuget
  • DiffPlex 1.7.0
  • Microsoft.NET.Test.Sdk 17.1.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/DafnyRuntime/DafnyRuntime.csproj nuget
  • System.Collections.Immutable 1.7.0
  • System.Runtime.Numerics 4.3.0
Source/DafnyRuntime/packages.config nuget
  • System.Collections.Immutable 1.7.0
  • System.Runtime 4.3.1
Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj nuget
  • Microsoft.NET.Test.Sdk 16.11.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/DafnyServer/DafnyServer.csproj nuget
Source/DafnyTestGeneration/DafnyTestGeneration.csproj nuget
Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj nuget
  • Microsoft.NET.Test.Sdk 17.1.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.extensibility.core 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/IntegrationTests/IntegrationTests.csproj nuget
  • Microsoft.NET.Test.Sdk 16.11.0
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.5.1
Source/TestDafny/TestDafny.csproj nuget
  • CommandLineParser 2.9.1
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.4.3
Source/XUnitExtensions/XUnitExtensions.csproj nuget
  • CommandLineParser 2.8.0
  • DiffPlex 1.7.0
  • Microsoft.Extensions.FileSystemGlobbing 5.0.0
  • Microsoft.NET.Test.Sdk 16.9.4
  • Xunit.SkippableFact 1.4.8
  • coverlet.collector 3.2.0
  • xunit 2.4.2
  • xunit.runner.visualstudio 2.4.3
Test/DafnyTests/DafnyTests.csproj nuget
Test/comp/manualcompile/ManualCompile.csproj nuget
Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj nuget
Test/comp/separate-compilation/consumer/Consumer.csproj nuget
Test/examples/Simple_compiler/csharp/SimpleCompiler.csproj nuget
  • Antlr4.CodeGenerator 4.6.6
  • antlr4.runtime 4.6.6
docs/Gemfile rubygems
  • github-pages ~> 228 development
  • jekyll-numbered-headings >= 0
  • kramdown >= 2.3.1
  • minima ~> 2.5
  • tzinfo ~> 2.0
  • tzinfo-data >= 0
  • wdm ~> 0.1.1
docs/Gemfile.lock rubygems
  • activesupport 7.0.7.2
  • addressable 2.8.4
  • bundler 2.4.13
  • coffee-script 2.4.1
  • coffee-script-source 1.11.1
  • colorator 1.1.0
  • commonmarker 0.23.10
  • concurrent-ruby 1.2.2
  • dnsruby 1.70.0
  • em-websocket 0.5.3
  • ethon 0.16.0
  • eventmachine 1.2.7
  • execjs 2.8.1
  • faraday 2.7.5
  • faraday-net_http 3.0.2
  • ffi 1.15.5
  • forwardable-extended 2.6.0
  • gemoji 3.0.1
  • github-pages 228
  • github-pages-health-check 1.17.9
  • html-pipeline 2.14.3
  • http_parser.rb 0.8.0
  • i18n 1.14.1
  • jekyll 3.9.3
  • jekyll-avatar 0.7.0
  • jekyll-coffeescript 1.1.1
  • jekyll-commonmark 1.4.0
  • jekyll-commonmark-ghpages 0.4.0
  • jekyll-default-layout 0.1.4
  • jekyll-feed 0.15.1
  • jekyll-gist 1.5.0
  • jekyll-github-metadata 2.13.0
  • jekyll-include-cache 0.2.1
  • jekyll-mentions 1.6.0
  • jekyll-numbered-headings 0.1.1
  • jekyll-optional-front-matter 0.3.2
  • jekyll-paginate 1.1.0
  • jekyll-readme-index 0.3.0
  • jekyll-redirect-from 0.16.0
  • jekyll-relative-links 0.6.1
  • jekyll-remote-theme 0.4.3
  • jekyll-sass-converter 1.5.2
  • jekyll-seo-tag 2.8.0
  • jekyll-sitemap 1.4.0
  • jekyll-swiss 1.0.0
  • jekyll-theme-architect 0.2.0
  • jekyll-theme-cayman 0.2.0
  • jekyll-theme-dinky 0.2.0
  • jekyll-theme-hacker 0.2.0
  • jekyll-theme-leap-day 0.2.0
  • jekyll-theme-merlot 0.2.0
  • jekyll-theme-midnight 0.2.0
  • jekyll-theme-minimal 0.2.0
  • jekyll-theme-modernist 0.2.0
  • jekyll-theme-primer 0.6.0
  • jekyll-theme-slate 0.2.0
  • jekyll-theme-tactile 0.2.0
  • jekyll-theme-time-machine 0.2.0
  • jekyll-titles-from-headings 0.5.3
  • jekyll-watch 2.2.1
  • jemoji 0.12.0
  • kramdown 2.3.2
  • kramdown-parser-gfm 1.1.0
  • liquid 4.0.4
  • listen 3.8.0
  • mercenary 0.3.6
  • mini_portile2 2.8.2
  • minima 2.5.1
  • minitest 5.19.0
  • nokogiri 1.14.3
  • octokit 4.25.1
  • pathutil 0.16.2
  • public_suffix 4.0.7
  • racc 1.6.2
  • rb-fsevent 0.11.2
  • rb-inotify 0.10.1
  • rexml 3.2.5
  • rouge 3.26.0
  • ruby2_keywords 0.0.5
  • rubyzip 2.3.2
  • safe_yaml 1.0.5
  • sass 3.7.4
  • sass-listen 4.0.0
  • sawyer 0.9.2
  • simpleidn 0.2.1
  • terminal-table 1.8.0
  • typhoeus 1.4.0
  • tzinfo 2.0.6
  • tzinfo-data 1.2023.3
  • unf 0.1.4
  • unf_ext 0.0.8.2
  • unicode-display_width 1.8.0
  • wdm 0.1.1
.github/workflows/nightly-build-manual.yml actions
.github/workflows/nightly-build-reusable.yml actions
  • actions/checkout v3 composite
.github/workflows/nightly-build.yml actions