MCP Z3 Prover

Name: MCP Z3 Prover
Author: daedalus

โดย daedalusรุ่น 0.1.0i★ –iรันบนเครื่อง

ชื่อใน registryio.github.daedalus/mcp-z3-prover

ติดตั้ง

ภาพรวม

คำอธิบายจากผู้ทำ (ภาษาอังกฤษตามต้นฉบับ)

MCP server exposing Z3 solver API

สามเสาของ PopNx MCP

สามเรื่องนี้ไม่รวมเป็นคะแนนเดียว เพราะความเห็น การวัด และความนิยม เป็นคนละเรื่องกัน

เสียงผู้ใช้iยังไม่มีรีวิวรีวิวเปิดพร้อมระบบบัญชีในขั้นถัดไป
ผลตรวจเบื้องต้นของเราiผ่าน 1 จาก 1 ข้อตรวจจากข้อมูลที่เปิดอยู่ ยังไม่ได้สแกนโค้ด
การใช้งานiยังไม่ได้วัด★ –

ใช้ทำอะไรได้

ตัวนี้ยังไม่ได้เรียบเรียงเป็นภาษาไทย ด้านล่างคือข้อเท็จจริงที่เราอ่านจาก registry

การเชื่อมต่อ: รันบนเครื่อง
ช่องทาง (transport): stdio
หมวด: อื่น ๆ

ติดตั้ง

เลือกโปรแกรม AI ที่คุณใช้ แล้วคัดลอกค่าตั้งไปวาง

ก่อนติดตั้ง

ผลตรวจเบื้องต้น: ผ่าน 1 จาก 1 ข้อ
รันในเครื่องคุณด้วยสิทธิ์ของผู้ใช้คุณ (ไฟล์ อินเทอร์เน็ต แอปต่าง ๆ)
ทะเบียนไม่ได้ระบุ key ที่ต้องใส่

ต้องเตรียมก่อน

PyPIติดตั้ง uv ของ Python (มีคำสั่ง uvx) ในเครื่อง

คุณใช้แอปไหน

ClaudeClaude CodeCursorVS CodeChatGPT

เลือกแอปด้านบน เราจำไว้ให้ ครั้งหน้าปุ่มจะขึ้นว่า “ติดตั้งลง …”

เปิด Claude Desktop → Settings → Developer → Edit Config แล้ววางค่านี้ในไฟล์ claude_desktop_config.json

{
  "mcpServers": {
    "z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

พิมพ์คำสั่งนี้ใน Terminal

claude mcp add z3-prover -- uvx mcp-z3-prover

เปิดใน Cursor

หรือคัดลอกค่าตั้งเอง

วางในไฟล์ .cursor/mcp.json ของโปรเจกต์ หรือ ~/.cursor/mcp.json

{
  "mcpServers": {
    "z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

เบราว์เซอร์จะถามก่อนเปิดแอป จากนั้นแอปแสดงค่าตั้งให้ตรวจแล้วกดยืนยัน ช่อง key เว้นว่างไว้ให้คุณใส่เอง

เปิดใน VS Code

หรือคัดลอกค่าตั้งเอง

วางในไฟล์ .vscode/mcp.json ของโปรเจกต์

{
  "servers": {
    "z3-prover": {
      "type": "stdio",
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

ตัวนี้รันในเครื่องคุณ แต่ ChatGPT ต่อได้เฉพาะ server บนอินเทอร์เน็ต ลองเลือกแอปอื่น

ตัวเลือกเก็บในคุกกี้บนเครื่องนี้ ไม่ต้องมีบัญชี

ค่าตั้งนี้สร้างจากข้อมูลใน registry ของผู้ทำ ถ้าไม่ตรงกับ README ให้เชื่อ README

ทำอะไรได้บ้าง

รันในเครื่องคุณ รายการเครื่องมือจะขึ้นในแอป AI หลังติดตั้ง

ผลตรวจเบื้องต้นi

เราตรวจจากข้อมูลที่ใครก็เปิดดูได้ ยังไม่ได้อ่านโค้ด ข้อที่ไม่เกี่ยวกับตัวนี้ไม่นับในตัวหาร · ตรวจเมื่อ 7 พ.ย. 2569

✓ ผ่าน
ตัวตนผู้ทำตรงกับ repo
ชื่อใน registry ยืนยันด้วยบัญชี GitHub daedalus ซึ่งเป็นเจ้าของ repo
… ยังไม่ตรวจ
ยังมีคนดูแล
ยังไม่ได้อ่านข้อมูล repo จาก GitHub
… ยังไม่ตรวจ
มีสัญญาอนุญาต (license)
ยังไม่ได้อ่านข้อมูล repo จาก GitHub
– ไม่เกี่ยว
endpoint ตอบ
ตัวนี้รันบนเครื่องคุณ ไม่มี endpoint บนอินเทอร์เน็ต
– ไม่เกี่ยว
ล็อกอินแบบ OAuth
ตัวนี้รันบนเครื่อง ใช้ค่าที่ตั้งในเครื่องแทน
… ยังไม่ตรวจ
คำอธิบายเครื่องมือไม่มีคำสั่งแอบแฝง
รันในเครื่องคุณ เราอ่านรายการเครื่องมือได้เฉพาะตัวที่มี endpoint บนอินเทอร์เน็ต

เทียบกับตัวอื่นในหมวด อื่น ๆi

ดาวมากกว่า 0% ของอีก 18333 ตัวในหมวดนี้
ส่งรุ่นใหม่เข้า registry ล่าสุดกว่า 4% ของอีก 18333 ตัวในหมวดนี้
ผลตรวจเบื้องต้นดีกว่าหรือเท่ากับ 100% ของอีก 18333 ตัวในหมวดนี้

เทียบกับทุก server ที่ยังใช้งานในหมวดนี้ทั้งทะเบียน ดาวนับเฉพาะเมื่อผู้ลงทะเบียนเป็นเจ้าของ repo

คำถามที่พบบ่อย

MCP Z3 Prover ปลอดภัยไหม?

จากการตรวจเบื้องต้นของเรา ผ่าน 1 จาก 1 ข้อที่ตรวจได้ เรายังไม่ได้อ่านโค้ด ก่อนใส่กุญแจหรือ token ให้ดูว่า server ขอสิทธิ์อะไร และเลือกกุญแจที่ทำได้เท่าที่จำเป็น

ต้องใช้กุญแจหรือรหัสอะไรบ้าง?

registry ไม่ได้ระบุว่าต้องใช้กุญแจ แต่บางตัวจะขอให้ล็อกอินตอนใช้ครั้งแรก

ตัวนี้รันบนเครื่องหรือบนคลาวด์?

รันบนเครื่องของคุณ โปรแกรม AI จะเปิด server ขึ้นมาเองเมื่อใช้ ข้อมูลไม่ต้องผ่านเซิร์ฟเวอร์ของผู้ทำ (ยกเว้นตัวที่ไปเรียกบริการออนไลน์ต่อ)

ยังมีคนดูแลอยู่ไหม?

repo บน GitHub มีการแก้โค้ดล่าสุด – และส่งรุ่นล่าสุด (0.1.0) เข้า registry 7 เดือนที่ผ่านมา

ใช้กับโปรแกรมไหนได้บ้าง?

โปรแกรมที่รองรับ MCP เช่น Claude Desktop, Claude Code, Cursor และ VS Code ตัวนี้ต้องมี Python (uv) ในเครื่องด้วย

มีตัวไหนใช้แทนได้บ้าง?

ในหมวดเดียวกันมี Spec Driven Development, Remote Desktop Commander, Signoff

ตัวที่ใช้แทนได้

server หมวดเดียวกันจากผู้ทำคนอื่น เรียงตามดาว

อ่านการ์ด:★ ดาว GitHubiสามเสา: รีวิว · ผลตรวจ · การใช้งานiอัปเดต = วันที่ส่งรุ่นล่าสุดเข้า registryi

Spec Driven Development

โดย formulahendry

MCP Server that facilitates spec-driven development workflows, not just Vibe Coding.

รันบนเครื่อง★ 440MITอัปเดต 14 เดือนที่ผ่านมา

ติดตั้ง

Remote Desktop Commander

โดย desktop-commander

Remote Desktop Commander: use files, terminal and processes on your own computers from any AI app.

รันบนคลาวด์★ 211อัปเดต เมื่อวานซืน

ติดตั้ง

Signoff

โดย ayuanxx-max

Five gates that make an agent's 'done' provable: run them, read the verdict, audit the record.

รันบนเครื่องอัปเดต วันนี้

ติดตั้ง

README จากผู้ทำ

เปิดอ่าน README

ส่วนนี้คัดจาก repo ของผู้ทำตามต้นฉบับ PopNx MCP ไม่ได้ตรวจหรือรับรองเนื้อหา ตัด HTML รูปภาพ และสคริปต์ออกแล้ว ลิงก์จะพาออกนอกเว็บ

mcp-z3-prover

MCP server exposing Z3 solver API

Install

pip install mcp-z3-prover

Usage

from mcp_z3_prover import mcp

Run the server

mcp.run()

Or from command line:

mcp-z3-prover

MCP Tools

The server exposes the following tools:

create_bool_var - Create a Boolean variable
create_int_var - Create an Integer variable
create_real_var - Create a Real variable
create_int_constant - Create an integer constant
create_real_constant - Create a real constant
add_constraint - Add a constraint to the solver
solve - Solve the current problem
get_model_value - Get value of a variable from the model
optimize - Solve with optimization objective
reset_solver - Reset the solver state
list_variables - List all created variables

Example

# Create variables

create_int_var("x") create_int_var("y")

Add constraints

add_constraint("int:x + int:y == 10") add_constraint("int:x > 0") add_constraint("int:y > 0")

Solve

result = solve()

Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

Get specific values

x_val = get_model_value("int:x")

Integer Factorization Example

# Factor n = 4295229443 where n = p * q with q <= sqrt(n)

create_int_var("p") create_int_var("q")

Add constraints

add_constraint("int:p * int:q == 4295229443") add_constraint("4295229443 > int:p") add_constraint("4295229443 > int:q") add_constraint("int:q <= 65537") # sqrt(4295229443) ≈ 65537 add_constraint("int:q > 1") add_constraint("int:p > 1") add_constraint("int:q % 2 != 0") # q is odd add_constraint("int:p % 2 != 0") # p is odd

Solve

result = solve()

Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}

Verification: 65537 * 65539 = 4295229443

Development

git clone https://github.com/daedalus/mcp-z3-prover.git

cd mcp-z3-prover pip install -e ".[test]"

run tests

pytest

format

ruff format src/ tests/

lint

ruff check src/ tests/

type check

mypy src/

MCP Registration

mcp-name: io.github.daedalus/mcp-z3-prover

MCP Z3 Prover

ภาพรวม

สามเสาของ PopNx MCP

ใช้ทำอะไรได้

ติดตั้ง

ก่อนติดตั้ง

ทำอะไรได้บ้าง

ผลตรวจเบื้องต้นi

ตัวตนผู้ทำตรงกับ repo

ยังมีคนดูแล

มีสัญญาอนุญาต (license)

endpoint ตอบ

ล็อกอินแบบ OAuth

คำอธิบายเครื่องมือไม่มีคำสั่งแอบแฝง

เทียบกับตัวอื่นในหมวด อื่น ๆi

คำถามที่พบบ่อย

ตัวที่ใช้แทนได้

Spec Driven Development

Remote Desktop Commander

Signoff

README จากผู้ทำ

mcp-z3-prover

Install

Usage

Run the server

MCP Tools

Example

Add constraints

Solve

Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

Get specific values

Integer Factorization Example

Add constraints

Solve

Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}

Verification: 65537 * 65539 = 4295229443

Development

run tests

format

lint

type check

MCP Registration