Use python library

.github/workflows/tests.yml

@@ -0,0 +1,40 @@
+name: Python integration
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: python-integration-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  test:
+    name: ${{ matrix.os }} / Python ${{ matrix.python }}
+    runs-on: ${{ matrix.os }}
+    timeout-minutes: 15
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-24.04, macos-latest, windows-latest]
+        python: ['3.10', '3.14']
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@v6
+        with:
+          python-version: ${{ matrix.python }}
+          cache: pip
+          cache-dependency-path: pyproject.toml
+      - name: Install with published Kepler Formal and NajaEDA wheels
+        run: python -m pip install --only-binary=kepler-formal,najaeda .
+      - name: Validate dependency versions
+        run: python -m pip check
+      - name: Test Python verification and MCP transport
+        run: python -m unittest discover -s tests -v

.gitignore

@@ -0,0 +1,7 @@
+.venv/
+__pycache__/
+*.py[cod]
+*.egg-info/
+build/
+dist/
+*.log

README.md

@@ -1,46 +1,84 @@
 # kepler-formal-mcp
 
-## Usage
+MCP tools for checking whether two Verilog designs are equivalent. NajaEDA loads the designs, then the published **Kepler Formal Python library** verifies them using the same native Naja runtime.
 
-To use this MCP, simply:
+## Install
 
-1. Clone the repository with submodules, or initialize the submodule afterward.
-2. Run the build script:
+Use CPython 3.10–3.14 on Linux x86_64/aarch64, macOS ARM64, or Windows AMD64, where the pinned dependencies provide wheels.
 
 ```bash
-./build_kepler_formal.sh
+git clone https://github.com/keplertech/kepler-formal-mcp.git
+cd kepler-formal-mcp
+python3 -m venv .venv
+source .venv/bin/activate
+python -m pip install --only-binary=kepler-formal,najaeda .
 ```
 
-If you also want the system dependencies to be installed automatically, run:
+On Windows, create and activate the environment with PowerShell:
+
+```powershell
+py -3 -m venv .venv
+.venv\Scripts\Activate.ps1
+python -m pip install --only-binary=kepler-formal,najaeda .
+```
+
+Installing this project installs `kepler-formal==0.5.0`, which requires `najaeda==0.7.24`, plus the MCP SDK and PyYAML. No Nix, submodule checkout, C++ build, or system compiler setup is needed.
+
+Start the stdio MCP server with:
 
 ```bash
-./build_kepler_formal.sh --install-deps
+kepler-formal-mcp
 ```
 
-This script will fetch `kepler-formal`, initialize its submodules, and then build the binary in `thirdparty/kepler-formal/build/`.
+The existing `python server.py` launcher also works using the installed environment. For desktop clients, use the absolute path to `.venv/bin/kepler-formal-mcp` (Windows: `.venv\Scripts\kepler-formal-mcp.exe`). See [Claude Desktop configuration](docs/instructions-claude.md).
 
-The repository now includes `kepler-formal` as a proper Git submodule in `thirdparty/kepler-formal`.
+## Tools
 
-After that, `server.py` automatically looks for the generated binary in the correct directory, so there is no extra manual step to locate it.
+- `get_kepler_formal_info`: report installed versions, build revision, and the available Python API options/results.
+- `run_kepler_formal_yaml`: verify the pair specified by an existing YAML file.
+- `create_yaml_and_run_kepler_formal`: create a YAML file from two Verilog paths and optional common Liberty libraries, then verify the pair.
 
-## Dependencies
+The tools use the Python library in a separate Python worker for each call. This keeps native solver output out of the MCP stdio channel and allows `timeout_seconds` to stop a verification. For verification, the worker loads both designs with NajaEDA and passes their live design handles to `kepler_formal.verify_designs`.
 
-On Linux Ubuntu/Debian:
+A minimal YAML file is:
 
-```bash
-sudo apt-get install g++ libboost-dev python3.9-dev capnproto libcapnp-dev libtbb-dev pkg-config bison flex doxygen libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
+```yaml
+format: verilog
+input_paths:
+  - reference.v
+  - candidate.v
+liberty_files: []
+verification: lec
+solver: kissat
+cnf_export: false
 ```
 
-On Fedora:
+Exactly two structural Verilog netlist files are required. Synthesize behavioral RTL before loading it with NajaEDA. Paths inside an existing YAML file are resolved relative to that file; paths passed to the create tool are resolved relative to the server's launch directory. The create tool writes absolute design/library paths into its generated YAML.
 
-```bash
-sudo dnf install gcc-c++ boost-devel python3-devel capnproto capnproto-devel tbb-devel pkgconf-pkg-config bison flex doxygen spdlog-devel fmt-devel boost-iostreams-devel zlib-devel cmake git
-```
+Set `KEPLER_FORMAL_AI_OUTPUT_DIR` to a writable output directory, or pass `allowed_output_dir` to a tool. The default is the server's launch directory. Generated YAML and logs must stay inside the selected output directory. An existing YAML file is read without rewriting it.
+
+Supported verification settings are `verification` (`lec` or `sec`; `mode` is an alias), `solver`, `max_k`, `sec_engine`, `sec_encoding`, `allow_boundary_mismatch`, `report_skipped_outputs`, `log_file`, and `log_level`. CNF export is unavailable through this library API: `cnf_export` defaults to `false`, and `true` returns a clear error. Unsupported CLI-only YAML options also return an error.
+
+All current `VerificationOptions` fields are exposed. See [Python API coverage and SEC usage](docs/python-api.md) for the mapping and supported choices. MCP tool schemas list the accepted modes, solvers, engines and encodings; `get_kepler_formal_info` reads them from the installed library.
+
+## Results
+
+The returned JSON separates tool execution from the verification verdict:
+
+- `status`: `success` when verification ran, or `error` for invalid input, timeout, or a worker failure.
+- `verdict`: the equivalence outcome, such as `equivalent`, `different`, or `inconclusive`.
+- `verification_result`: the structured result returned by Kepler Formal.
+- `stdout_tail` / `stderr_tail`: captured worker output for diagnosis.
+- `reports`: contents of native skipped-output reports, retained after worker cleanup when `report_skipped_outputs` is enabled.
+
+Always inspect `verdict`: a successful execution can report different designs. A bounded SEC check can be inconclusive; it is not an equivalence proof.
+
+See [the small design example](docs/test-generation.md) for equivalent and different inputs.
 
-On macOS with Homebrew:
+## Test
 
 ```bash
-brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
+python -m unittest discover -s tests -v
 ```
 
-On Windows, the easiest approach is to use WSL2 or MSYS2 with a compatible Bash environment. Automatic installation of system dependencies is not supported on native Windows.
+CI runs the tests against the published dependencies on Linux x86_64, macOS ARM64, and Windows AMD64 with Python 3.10 and 3.14. Tests cover every solver and SEC engine/encoding, API option/result coverage, diagnostic reports, configuration validation, worker isolation, and MCP stdio calls.

docs/instructions-claude.md

@@ -1,76 +1,45 @@
 # Configuring Kepler Formal MCP in Claude Desktop
 
-This guide explains how to add the Kepler Formal MCP server to Claude Desktop.
+First install the project in a virtual environment using the [README](../README.md). The environment includes the published Kepler Formal and NajaEDA packages.
 
-**Note:** This guide assumes you have already installed Kepler Formal MCP. See the main README and build script for installation instructions.
-
-## Configuration
-
-### Step 1: Locate Your Configuration File
-
-Find your Claude Desktop configuration file:
-- **Linux/Mac**: `~/.config/Claude/claude_desktop_config.json`
-- **Windows**: `%APPDATA%\Claude\claude_desktop_config.json`
-
-### Step 2: Add Kepler Formal to Your MCP Servers
-
-Edit your configuration file and add the Kepler Formal server. Replace the placeholders with your actual paths:
-- `<mcp-server-name>`: A name for this server (e.g., `kepler`, `kepler-formal`, `formal-verification`)
-- `<path-to-kepler-formal-mcp>`: Full path to your Kepler Formal MCP repository
-- `<path-to-kepler-formal-src>`: Path to the Kepler Formal source code (usually `<path-to-kepler-formal-mcp>/thirdparty/kepler-formal/src`)
+Add this entry to your Claude Desktop MCP configuration, replacing both paths with absolute paths on your machine:
 
 ```json
 {
   "mcpServers": {
-    "<mcp-server-name>": {
-      "command": "python3",
-      "args": [
-        "<path-to-kepler-formal-mcp>/server.py"
-      ],
+    "kepler-formal": {
+      "command": "/absolute/path/to/kepler-formal-mcp/.venv/bin/kepler-formal-mcp",
       "env": {
-        "PYTHONPATH": "<path-to-kepler-formal-src>"
+        "KEPLER_FORMAL_AI_OUTPUT_DIR": "/absolute/path/to/verification-output"
       }
     }
   }
 }
 ```
 
-### Step 3: Verify
-
-1. Save the configuration file
-2. Restart Claude Desktop
-3. Check that your MCP server appears as "Connected" in Claude's MCP server list
-
-## Strongly Recommended: Add a Shared Folder
-
-Adding a shared folder is strongly recommended. Without it, you'll need to copy-paste potentially large files directly into Claude's prompt, which is inefficient and can hit token limits.
-
-With the filesystem MCP server, Claude can access your files directly:
+On Windows, use the virtual environment's executable and JSON-escaped backslashes:
 
 ```json
-"filesystem": {
-  "command": "npx",
-  "args": [
-    "-y",
-    "@modelcontextprotocol/server-filesystem",
-    "<path-to-shared-folder>"
-  ]
+{
+  "mcpServers": {
+    "kepler-formal": {
+      "command": "C:\\absolute\\path\\kepler-formal-mcp\\.venv\\Scripts\\kepler-formal-mcp.exe",
+      "env": {
+        "KEPLER_FORMAL_AI_OUTPUT_DIR": "C:\\absolute\\path\\verification-output"
+      }
+    }
+  }
 }
 ```
 
-Replace `<path-to-shared-folder>` with an absolute path to a folder where you want to store files accessible to Claude. This allows Claude to read large design files, test vectors, and documentation without copy-pasting.
+No `PYTHONPATH` or Kepler Formal source directory is required. The executable uses its virtual environment even when Claude starts from another directory. Save the configuration and restart Claude Desktop.
+
+Use absolute design and library paths in tool calls because desktop clients may launch servers from an unexpected directory. The output environment variable controls where generated YAML and logs can be written; each call can override it with `allowed_output_dir`.
 
-## Troubleshooting
+For example:
 
-**Server won't connect:**
-- Verify paths are absolute (not relative)
-- Restart Claude Desktop after saving the config
-- Ensure the config file is valid JSON
-- Check that `<path-to-kepler-formal-mcp>/server.py` exists
+> Use `create_yaml_and_run_kepler_formal` to compare `/my/designs/reference.v` and `/my/designs/candidate.v`, with no Liberty libraries. Report the verification verdict.
 
-**"Command not found" for python3:**
-- Use the full path to Python: `/usr/bin/python3` instead of `python3`
+For an existing YAML file, paths inside it are relative to its directory. Ask Claude to use `run_kepler_formal_yaml` with the YAML file's absolute path. The MCP reads the designs directly; a filesystem MCP is only needed if you also want Claude to create or edit the design files.
 
-**Invalid JSON errors:**
-- Use a JSON validator to check your config file
-- Ensure all commas and quotes are correct
+If connection fails, check that the configured executable exists and that the environment was installed successfully with `python -m pip check`. Run the executable in a terminal to inspect errors on stderr. It normally waits silently for MCP messages on stdin.