# Directory Structure

```
├── .gitignore
├── LICENSE
├── mcp.py
└── README.md
```

# Files

--------------------------------------------------------------------------------
/.gitignore:
--------------------------------------------------------------------------------

```
# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class

# C extensions
*.so

# Distribution / packaging
.Python
build/
develop-eggs/
dist/
downloads/
eggs/
.eggs/
lib/
lib64/
parts/
sdist/
var/
wheels/
share/python-wheels/
*.egg-info/
.installed.cfg
*.egg
MANIFEST

# PyInstaller
#  Usually these files are written by a python script from a template
#  before PyInstaller builds the exe, so as to inject date/other infos into it.
*.manifest
*.spec

# Installer logs
pip-log.txt
pip-delete-this-directory.txt

# Unit test / coverage reports
htmlcov/
.tox/
.nox/
.coverage
.coverage.*
.cache
nosetests.xml
coverage.xml
*.cover
*.py,cover
.hypothesis/
.pytest_cache/
cover/

# Translations
*.mo
*.pot

# Django stuff:
*.log
local_settings.py
db.sqlite3
db.sqlite3-journal

# Flask stuff:
instance/
.webassets-cache

# Scrapy stuff:
.scrapy

# Sphinx documentation
docs/_build/

# PyBuilder
.pybuilder/
target/

# Jupyter Notebook
.ipynb_checkpoints

# IPython
profile_default/
ipython_config.py

# pyenv
#   For a library or package, you might want to ignore these files since the code is
#   intended to run in multiple environments; otherwise, check them in:
# .python-version

# pipenv
#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
#   However, in case of collaboration, if having platform-specific dependencies or dependencies
#   having no cross-platform support, pipenv may install dependencies that don't work, or not
#   install all needed dependencies.
#Pipfile.lock

# UV
#   Similar to Pipfile.lock, it is generally recommended to include uv.lock in version control.
#   This is especially recommended for binary packages to ensure reproducibility, and is more
#   commonly ignored for libraries.
#uv.lock

# poetry
#   Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
#   This is especially recommended for binary packages to ensure reproducibility, and is more
#   commonly ignored for libraries.
#   https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
#poetry.lock

# pdm
#   Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
#pdm.lock
#   pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
#   in version control.
#   https://pdm.fming.dev/latest/usage/project/#working-with-version-control
.pdm.toml
.pdm-python
.pdm-build/

# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
__pypackages__/

# Celery stuff
celerybeat-schedule
celerybeat.pid

# SageMath parsed files
*.sage.py

# Environments
.env
.venv
env/
venv/
ENV/
env.bak/
venv.bak/

# Spyder project settings
.spyderproject
.spyproject

# Rope project settings
.ropeproject

# mkdocs documentation
/site

# mypy
.mypy_cache/
.dmypy.json
dmypy.json

# Pyre type checker
.pyre/

# pytype static type analyzer
.pytype/

# Cython debug symbols
cython_debug/

# PyCharm
#  JetBrains specific template is maintained in a separate JetBrains.gitignore that can
#  be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
#  and can be added to the global gitignore or merged into this file.  For a more nuclear
#  option (not recommended) you can uncomment the following to ignore the entire idea folder.
#.idea/

# PyPI configuration file
.pypirc

```

--------------------------------------------------------------------------------
/README.md:
--------------------------------------------------------------------------------

```markdown
# dafny-mcp
Dafny Verifier Tool for the Model Context Protocol, which can be used with Claude

## Dependencies

- Uses Dafny locally so install it, e.g. `brew install dafny` on Mac OS X.
- Uses the [MCP Python SDK](https://github.com/modelcontextprotocol/python-sdk)


## Setup

- `uv pip install "mcp[cli]"`
- `mcp install mcp.py`
- `mcp dev mcp.py`

```

--------------------------------------------------------------------------------
/mcp.py:
--------------------------------------------------------------------------------

```python
import hashlib
import os
from mcp.server.fastmcp import FastMCP

mcp = FastMCP("Dafny")

@mcp.tool()
def dafny_verifier(code: str) -> str:
    """Verify a Dafny code."""
    t = 2 # timeout
    v = code

    TMP_DIR = '/tmp/dafny/'
    
    if t is None:
        t = 10
    key = hashlib.md5(v.encode('utf-8')).hexdigest()
    dir = "%s%s/" % (TMP_DIR, key)
    if not os.path.exists(dir):
        os.makedirs(dir)
    os.chdir(dir)

    fn = 'ex.dfy'
    outfn = 'out.txt'
    errfn = 'err.txt'

    f = open(fn, 'w')
    f.write(v)
    f.close()
    
    status = os.system("dafny verify %s --verification-time-limit %s >%s 2>%s" % (fn, t, outfn, errfn))
    f = open(outfn, 'r')
    outlog = f.read()
    f.close()

    f = open(errfn, 'r')
    log = f.read()
    f.close()

    r = {'status': status, 'log': log, 'out': outlog[:1000]}
    return r['out']

```