Dafny Verifier

🚀 达芬尼-MCP

达芬尼验证工具用于模型上下文协议，可与Claude协同使用，为模型验证提供有力支持。

🚀 快速开始

依赖项

• 需使用本地Dafny，请进行安装，例如在Mac OS X系统上可执行 brew install dafny 进行安装。
• 需使用模型上下文协议Python SDK。

设置

• 执行 uv pip install "mcp[cli]"
• 执行 mcp install mcp.py
• 执行 mcp dev mcp.py

📦 安装指南

安装依赖

• 若使用Mac OS X系统，可通过Homebrew安装Dafny，命令如下：

brew install dafny

• 需从GitHub获取模型上下文协议Python SDK。

项目安装

依次执行以下命令进行项目安装与开发环境配置：

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