PeasyAI - AI for P

PeasyAI: AI-Assisted P Development

PeasyAI is an AI-powered code generation, compilation, and formal verification assistant for the P programming language. It exposes an MCP (Model Context Protocol) server that works with Cursor and Claude Code, providing 27 tools and 14 resources for generating P state machines from design documents, compiling them, and verifying correctness with PChecker.

Features

Design Doc to Verified P Code — Generate types, state machines, safety specs, and test drivers from a plain-text design document
Multi-Provider LLM Support — Snowflake Cortex, AWS Bedrock, Direct Anthropic
Ensemble Generation — Best-of-N candidate selection for higher quality code
Auto-Fix Pipeline — Automatically fix compilation errors and PChecker failures
Human-in-the-Loop — Falls back to user guidance when automated fixing fails
RAG-Enhanced — 1,200+ indexed P code examples improve generation quality

Prerequisites

PeasyAI relies on the P toolchain at runtime to compile and model-check your programs:

Dependency	Why it's needed	Install
Python >= 3.10	Runs the PeasyAI MCP server	python.org/downloads
.NET SDK, Java, and P compiler	Compiles and model-checks P programs	P installation guide

Verify your setup:

python3 --version          # >= 3.10
dotnet --list-sdks         # must show 8.0.*
java -version              # >= 11
p --version                # P compiler is on PATH

Installation

Install the latest release directly from GitHub:

pip install https://github.com/p-org/P/releases/download/peasyai-v1.0.0/peasyai_mcp-1.0.0-py3-none-any.whl

Check the Releases page for the latest version.

To upgrade to a newer release:

pip install --force-reinstall https://github.com/p-org/P/releases/download/peasyai-v<VERSION>/peasyai_mcp-<VERSION>-py3-none-any.whl

Alternative: install from source (for development)

git clone https://github.com/p-org/P.git
cd P/Src/PeasyAI
pip install -e ".[dev]"

Configuration

Run the init command to create the configuration file:

peasyai-mcp init

This creates ~/.peasyai/settings.json. Open it and fill in the credentials for the LLM provider you want to use:

{
  "llm": {
    "provider": "snowflake",
    "model": "claude-sonnet-4-5",
    "timeout": 600,
    "providers": {
      "snowflake": {
        "api_key": "your-snowflake-pat-token",
        "base_url": "https://your-account.snowflakecomputing.com/api/v2/cortex/openai"
      },
      "anthropic": {
        "api_key": "your-anthropic-key",
        "model": "claude-3-5-sonnet-20241022"
      },
      "bedrock": {
        "region": "us-west-2",
        "model_id": "anthropic.claude-3-5-sonnet-20241022-v2:0"
      }
    }
  },
  "generation": {
    "ensemble_size": 3,
    "output_dir": "./PGenerated"
  }
}

Only fill in the provider you use. Set provider to snowflake, anthropic, or bedrock.

Verify everything is set up correctly:

peasyai-mcp config

Configuration Reference

Key	Example	Description
`llm.provider`	`"snowflake"`	Active provider: `snowflake`, `anthropic`, or `bedrock`
`llm.model`	`"claude-sonnet-4-5"`	Model name (uses provider default if omitted)
`llm.timeout`	`600`	Request timeout in seconds
`llm.providers.snowflake.api_key`		Snowflake Programmatic Access Token
`llm.providers.snowflake.base_url`		Snowflake Cortex endpoint URL
`llm.providers.anthropic.api_key`		Anthropic API key
`llm.providers.bedrock.region`	`"us-west-2"`	AWS region
`llm.providers.bedrock.model_id`		Bedrock model ID
`generation.ensemble_size`	`3`	Best-of-N candidates per file
`generation.output_dir`	`"./PGenerated"`	Default output directory

Precedence: Environment variables > ~/.peasyai/settings.json > built-in defaults.

LLM Providers

Snowflake CortexAnthropic (Direct API)AWS Bedrock

Log into your Snowflake account
Go to Admin > Security > Programmatic Access Tokens
Create a token with Cortex API permissions
Set "provider": "snowflake" and fill in api_key and base_url

Set "provider": "anthropic" and fill in api_key.

Ensure ~/.aws/credentials is configured, then set "provider": "bedrock".

Add to Cursor

Edit ~/.cursor/mcp.json (create the file if it doesn't exist):

{
  "mcpServers": {
    "peasyai": {
      "command": "peasyai-mcp",
      "args": []
    }
  }
}

Restart Cursor — the PeasyAI tools will appear in the MCP panel.

Add to Claude Code

claude mcp add peasyai -- peasyai-mcp

MCP Tools

PeasyAI provides 27 MCP tools organized by category:

Category	Tool	Description
Generation	`peasy-ai-create-project`	Create P project skeleton (PSrc/, PSpec/, PTst/)
	`peasy-ai-gen-types-events`	Generate types, enums, and events file
	`peasy-ai-gen-machine`	Generate a single state machine (two-stage, ensemble)
	`peasy-ai-gen-spec`	Generate safety specification / monitor
	`peasy-ai-gen-test`	Generate test driver
	`peasy-ai-gen-full-project`	One-shot full project generation
	`peasy-ai-save-file`	Save generated code to disk
Compilation	`peasy-ai-compile`	Compile a P project
	`peasy-ai-check`	Run PChecker model-checking verification
Fixing	`peasy-ai-fix-compile-error`	Fix a single compilation error
	`peasy-ai-fix-checker-error`	Fix a PChecker error from trace analysis
	`peasy-ai-fix-all`	Iteratively fix all compilation errors
	`peasy-ai-fix-bug`	Auto-diagnose and fix PChecker failures
Workflows	`peasy-ai-run-workflow`	Execute a multi-step workflow (compile_and_fix, full_verification, etc.)
	`peasy-ai-resume-workflow`	Resume a paused workflow with user guidance
	`peasy-ai-list-workflows`	List available and active workflows
Query	`peasy-ai-syntax-help`	P language syntax help by topic
	`peasy-ai-list-files`	List all .p files in a project
	`peasy-ai-read-file`	Read contents of a P file
RAG	`peasy-ai-search-examples`	Search the P program database
	`peasy-ai-get-context`	Get examples to improve generation quality
	`peasy-ai-index-examples`	Index your own P files into the corpus
	`peasy-ai-get-protocol-examples`	Get examples for common protocols (Paxos, Raft, etc.)
	`peasy-ai-corpus-stats`	Get corpus statistics
Trace	`peasy-ai-explore-trace`	Explore a PChecker execution trace
	`peasy-ai-query-trace`	Query machine state at a point in the trace
Environment	`peasy-ai-validate-env`	Check P toolchain, LLM provider, and config

MCP Resources

Resource URI	Description
`p://guides/syntax`	Complete P syntax reference
`p://guides/basics`	P language fundamentals
`p://guides/machines`	State machine patterns
`p://guides/types`	Type system guide
`p://guides/events`	Event handling guide
`p://guides/enums`	Enum types guide
`p://guides/statements`	Statements and expressions guide
`p://guides/specs`	Specification monitors guide
`p://guides/tests`	Test cases guide
`p://guides/modules`	Module system guide
`p://guides/compiler`	Compiler usage guide
`p://guides/common_errors`	Common compilation errors and fixes
`p://examples/program`	Complete P program example
`p://about`	About the P language

Typical Workflow

The recommended step-by-step workflow for generating verified P code:

Create project — peasy-ai-create-project(design_doc, output_dir)
Generate types — peasy-ai-gen-types-events(design_doc, project_path) then review and peasy-ai-save-file
Generate machines — peasy-ai-gen-machine(name, design_doc, project_path) for each machine, then review and peasy-ai-save-file
Generate spec — peasy-ai-gen-spec("Safety", design_doc, project_path) then review and peasy-ai-save-file
Generate test — peasy-ai-gen-test("TestDriver", design_doc, project_path) then review and peasy-ai-save-file
Compile — peasy-ai-compile(project_path)
Fix errors — peasy-ai-fix-all(project_path) if compilation fails
Verify — peasy-ai-check(project_path) to run PChecker
Fix bugs — peasy-ai-fix-bug(project_path) if PChecker finds issues

Or use peasy-ai-run-workflow("full_verification", project_path) to automate steps 6-9.

Human-in-the-Loop Error Fixing

The peasy-ai-fix-compile-error and peasy-ai-fix-checker-error tools try up to 3 automated fixes. If all fail, they return needs_guidance: true with diagnostic questions. Call the tool again with user_guidance containing the user's hint:

peasy-ai-fix-compile-error(...)             # attempt 1 — fails
peasy-ai-fix-compile-error(...)             # attempt 2 — fails
peasy-ai-fix-compile-error(...)             # attempt 3 — fails, returns needs_guidance=true
Ask user for guidance
peasy-ai-fix-compile-error(user_guidance="The type should be…")  # succeeds

Troubleshooting

Problem	Fix
`peasyai-mcp: command not found`	Make sure the pip install location is on your `PATH`. Try `python -m site --user-base` to find it, or use `pipx install` instead.
`p: command not found`	Install the P compiler following the P installation guide and ensure `~/.dotnet/tools` is on your `PATH`.
`dotnet: command not found`	Install .NET SDK 8.0 following the P installation guide.
MCP server not showing in Cursor	Restart Cursor after editing `~/.cursor/mcp.json`. Check the MCP panel for error messages.
LLM calls failing	Run `peasyai-mcp config` to verify your credentials are loaded correctly.