crs-mcp

당신의 패치를 작성한 에이전트는 자신의 과제를 채점할 수 없습니다.

지금 바로 설치 없이 시도하세요: 브라우저 데모 열기 및 위조본 로드를 누르세요 — 검사기가 클라이언트 측에서 이를 거부합니다.

AI 코딩 에이전트가 우회할 수 없는 평결 인터페이스를 제공하는 MCP 서버입니다. 에이전트가 가드를 제안하면, 이 서버는 해당 가드가 실제로 건전한지 판단하고, 그렇지 않을 경우 구체적인 반례를 돌려줍니다.

pip install "crs-mcp@git+https://github.com/nickharris808/crs-mcp@main"

사전 릴리스. PyPI 이름은 예약되어 있으며 곧 배포될 예정입니다. 그때까지 위 줄이 실제 설치 방법입니다. Linux, macOS, Windows에서 CI로 테스트되었습니다.

30초 퀵스타트

이것을 Claude Desktop (claude_desktop_config.json) 또는 Cursor에 추가하세요:

{
  "mcpServers": {
    "crs": {
      "command": "crs-mcp"
    }
  }
}

그런 다음 에이전트에게 물어보세요: "이 읽기 전에 경계 검사 1 + payload <= record_len를 추가했습니다. 이것을 3 + payload <= record_len에 대해 인증하세요."

{
  "verdict": "PROVEN_UNSOUND",
  "summary": "The guard admits 509 state(s) the safety property forbids (out of 65,536). Example: {'record_len': 1, 'payload': 0}.",
  "detail": {
    "over_acceptance": 509,
    "box_volume": 65536,
    "counterexample": {"record_len": 1, "payload": 0},
    "hit_probability": 0.0077667236328125,
    "expected_draws_to_hit": 128.75442043222003
  }
}

그것은 실제 반례입니다: payload=0, record_len=1에서 가드는 통과하지만 안전 속성은 성립하지 않습니다. 에이전트는 그것에 대해 논쟁할 수 없고, 당신도 마찬가지입니다.

Related MCP server: Chiasmus

세 가지 평결

OUT_OF_SCOPE가 중요한 것입니다. 실패가 아니며 단호히 통과도 아닙니다. 에이전트는 "오류 없음"을 "승인"으로 읽고 커밋할 것입니다; 도구 설명은 그런 해석을 막기 위해 작성되었으며, explain_refusal은 *"이것을 승인으로 취급하지 마십시오"*라는 말을 그대로 담은 문장을 반환합니다. 오직 초록색만 반환하는 도구는 도구가 없는 것보다 나쁩니다.

도구

verify_certificate는 추가로 certificate_verdict를 반환합니다. 이는 certkit 자체의 ACCEPTED / REFUSED / UNVERIFIED입니다. 확인에 실패한 인증서는 OUT_OF_SCOPE로 보고되며, 결코 PROVEN_UNSOUND로 보고되지 않습니다: 잘못된 증명은 증거의 부재이지, 불건전함의 증거가 아닙니다. 오직 상태를 세는 것만 가드의 불건전함을 증명할 수 있으며, 이것이 certify_guard가 하는 일입니다.

decide_guard: 더 빨리 얻는 동일한 답

대부분의 경우 에이전트는 *이것이 안전한가?*를 묻지 *얼마나 안전하지 않은가?*를 묻지 않습니다. decide_guard는 전체 영역을 세는 대신 첫 번째 탈출 상태에서 멈춥니다. 불건전한 가드에서 측정한 결과:

exploit-counter 저장소에서 python benchmarks/decide_vs_count.py로 다시 생성할 수 있습니다. 여기서 계산이 이루어집니다. 격차는 박스가 커질수록 증가합니다. 계산은 전체 위반 영역을 열거하고, 결정은 첫 번째 탈출 상태에서 멈추기 때문입니다.

동일한 판정 — 테스트는 150개의 랜덤 스펙에서 두 방법이 일치함을 확인합니다. 건전한 가드의 경우 두 방법 모두 동일한 비용이 듭니다. 건전성을 확립하려면 전체 열거가 진정으로 필요하기 때문입니다.

결과에는 over_acceptance 필드가 없습니다. 아무것도 세지 않았으므로, 거기에 숫자를 보고하는 것은 (0이라도) 분석이 생성하지 않은 수치가 될 것입니다.

결정 방법과 정직한 한계

인증은 당신이 선언한 박스에 대한 철저한 정수 계산으로 이루어집니다. 그것은 그 박스에 대해 건전하고 완전합니다 — 그리고 박스 밖에 대해서는 아무것도 말하지 않습니다. 그래서 박스는 컨텍스트에서 추론되는 것이 아니라 필수 인수입니다.

카운터는 가장 넓은 변수를 제외한 모든 변수를 열거하며, 가장 넓은 변수는 닫힌 형태로 풉니다. 따라서 비용은 다른 범위들의 곱이며, 상한은 그 곱에 적용됩니다 — 박스 부피가 아니라. 한계는 500,000개의 열거 포인트입니다. 이 머신에서 측정한 결과:

밀리초 열은 한 머신에서 나온 것이며 당신의 머신에서는 다를 수 있습니다. python benchmarks/ceiling.py를 실행하면 당신의 머신에서 이 표를 다시 생성합니다. 부피, 열거된 수, 판정은 정확하며 머신과 무관합니다.

상한 내의 모든 결정은 0.25초 미만으로 완료되므로 에이전트 호출이 멈추지 않습니다. 이전에는 그렇지 않았습니다: 최악의 경우를 프로파일링한 결과 시간의 ~70%가 Python의 Fraction 타입에서 소비되었기 때문에, exploit-counter는 이제 모든 계수가 정수일 때(모든 경계 관계가 그렇습니다) 정수 전용 내부 루프를 사용합니다. 정수는 유리수의 부분집합이므로 이것은 동일한 산술입니다 — 더 빠른 근사가 아니라 — 그리고 test_integer_and_rational_paths_agree는 두 구현을 서로 비교하여 확인합니다.

가장 밀집된 형태에서 1,491.2 ms → 244.6 ms입니다; 측정된 세 가지 형태 전체에서 중앙값 6.06x, 관찰된 3.55x–10.25x입니다. 형태당 11회의 짝지은 반복, 모든 반복에서 비트 단위로 동일한 결과. make bench-fast-path로 다시 생성하세요; 숫자는 이 페이지가 아닌 커밋된 artifacts/crs/bench_fast_path.json에서 나옵니다. 중앙값을 인용하세요 — 범위는 머신 부하와 문제 형태에 따라 움직이므로, 좁은 범위는 반복해서 말하기에 오해를 부르는 숫자입니다.

python benchmarks/ceiling.py로 재현하세요 — 그 스크립트는 정확히 이 표를 생성하며, 위의 숫자는 실제 출력입니다. 타이밍은 머신에 의존합니다; 판정과 열거된 수는 그렇지 않습니다.

사람들이 잘못 추측하는 두 가지 결과를 명확히 언급할 가치가 있습니다 — 그리고 이 README의 이전 버전이 두 가지 모두 틀렸기 때문입니다:

• 전체 2^32를 포함하는 두 변수 박스는 결정됩니다, 0.5초 미만으로. 이 README는 이전에 거부될 것이라고 주장했습니다.

• 가장 넓은 변수를 좁히는 것은 도움이 되지 않습니다. 이미 자유롭습니다. OUT_OF_SCOPE가 발생하면 다른 변수 중 하나를 좁히세요; 거부 메시지는 어떤 변수가 자유 변수인지 알려줍니다.

세 개 이상의 변수에서 전체 32비트 도메인을 결정하려면 열거하지 않는 결정 절차가 필요합니다 — 재생 가능한 인증서를 가진 솔버 없는 제거 방법. 그 절차는 이 패키지에 포함되어 있지 않습니다. 이 계층은 열거할 수 있는 박스에 대해 실제 판정을 제공하고, 열거할 수 없는 박스에 대해서는 정직한 거부를 제공합니다.

전체 머신 워드 도메인에 대한 판정이 필요하다면, 그것은 상용 제공입니다.

도구가 거부하는 질문

질문이 반대 방향으로 나올 수 있을 때만 판정은 가치가 있습니다. 다음은 답변 대신 OUT_OF_SCOPE로 거부됩니다:

각 거부는 문제가 되는 변수를 명명하고 무엇을 변경해야 하는지 알려줍니다.

Python에서 사용

도구 계층은 전송에 독립적이므로 MCP 없이도 호출할 수 있습니다:

from crs_mcp import certify_guard

v = certify_guard(
    domain=[{"coeff": {"payload": -1}}, {"coeff": {"payload": 1}, "const": -255}],
    guard=[{"coeff": {"payload": 1, "record_len": -1}, "const": 19}],
    safety=[{"coeff": {"payload": 1, "record_len": -1}, "const": 3}],
    box={"payload": [0, 255], "record_len": [0, 255]},
)
print(v.verdict)  # CERTIFIED

원자는 일반 정수(모델이 생성할 것) 또는 디스크의 certkit 형식의 [분자, 분모] 쌍을 허용합니다.

MCP가 아니어도 도구는 작동합니다

MCP는 이 패키지가 중심으로 구축된 전송이지만, 도구는 JSON을 받아 JSON을 반환하는 함수일 뿐입니다. 그것들에 대해 프레임워크나 서버가 필요하지 않습니다:

from crs_mcp import call, openai_tools, anthropic_tools, json_schemas

call("decide_guard", {"guard": [...], "safety": [...], "box": {...}})   # run one, no server
openai_tools()       # OpenAI function-calling schema, for `tools=`
anthropic_tools()    # Anthropic tool-use schema (input_schema, not parameters)
json_schemas()       # standalone JSON Schema documents, one per tool

python -m crs_mcp.adapters anthropic > tools.json    # paste into an agent config

LangChain 사용자는 crs_mcp.adapters.langchain_tools()를 얻습니다. LangChain은 이 패키지의 의존성이 아닙니다; 함수는 호출 시 그것을 임포트하며, 없으면 부분 통합을 조용히 반환하는 대신 설치 지침과 함께 예외를 발생시킵니다.

이 모든 것은 하나의 카탈로그(crs_mcp.catalog)에서 생성되며, 이는 표준 라이브러리 외에는 아무것도 임포트하지 않습니다 — 스키마는 이전에 MCP 서버 모듈 내부에 있었고, 따라서 mcp가 설치되어 있지 않으면 접근할 수 없었습니다.

설명은 중요한 역할을 합니다. 각 설명은 판정이 확립하지 않는 것을 명시합니다. 왜냐하면 OUT_OF_SCOPE를 "문제 없음"으로 읽는 에이전트는 안전하지 않은 코드를 병합할 것이기 때문입니다. 이름과 스키마를 유지하면서 그 문장을 생략한 어댑터는 완벽하게 올바른 것처럼 보일 수 있으므로, check_descriptions_intact()가 존재하며 모든 어댑터의 출력이 이에 대해 테스트됩니다. 어떤 어댑터도 OUT_OF_SCOPE를 불리언, 점수, 또는 통과로 매핑하지 않습니다.

지원되는 MCP 버전

mcp 1.9.0부터 1.29.0까지 검증되었으며, >=1.9.0,<2.0.0으로 고정되었습니다.

mcp 2.0.0은 서버 데코레이터 API를 변경했습니다 (Server.list_tools는 더 이상 존재하지 않음) 그리고 아직 지원되지 않습니다 — CI가 2.0.0 출시 당일에 이를 발견했습니다. 2.x 지원은 여기서 주장되지 않고 향후 작업으로 추적됩니다.

범위

• 선형 정수 산술만 지원. 비선형 항, 힙 형태, 별칭은 이 프래그먼트에서 제외됩니다. 도구는 그렇지 않은 것처럼 가장하지 않습니다.

• 수는 트리거 가능성이며, 심각도가 아닙니다. 균일 샘플링 아래에서 금지된 상태의 도달 가능성을 제한합니다. CVSS도 아니고 무기화 가능성 주장도 아닙니다.

• CERTIFIED는 박스로 제한됩니다. 실제 도메인에 대한 실제 증명이며, 그 도메인 밖의 모든 것에 대해 침묵합니다.

관련

• certkit — 인증서 형식 및 독립 검사기

• exploit-counter — 그 아래의 계산 엔진

테스트

pip install -e ".[dev]"
pytest

252개의 테스트. test_tools.py는 평결(verdict) 의미론을 다루고, test_server.py는 등록된 핸들러를 통해 실제 tools/list 및 tools/call 왕복을 수행합니다. 왜냐하면 툴 함수는 완벽하지만 핸들러가 잘못 등록된 서버는 다른 파일의 모든 테스트를 통과할 수 있기 때문입니다.

test_adversarial.py에는 가장 중요한 테스트가 들어 있습니다. 그 오라클은 한 문장입니다 — 어떤 입력도 자신만만해 보이는 틀린 답변을 만들어내서는 안 된다 — 그리고 에이전트가 "승인됨, 커밋하라"로 읽는 단어이기 때문에 CERTIFIED를 구체적으로 공격합니다. 또한 차등(differential) 테스트도 포함합니다: certkit과 exploit-counter는 동일한 질문에 대한 독립적인 구현(합리적 반박 산술 vs. 정수 열거)이며, 둘 다 모든 입력에 대해 무차별 대입(brute force)과 교차 검증됩니다. 둘 사이의 불일치는 틀린 쪽의 건전성(soundness) 버그입니다.

문서

툴킷의 나머지

폐쇄된 핵심(closed core)

이 패키지들은 검증 절반입니다. 여기에는 의도적으로 증명 탐색(proof search)이 포함되어 있지 않으며, 이것이 감사(audit) 가능할 만큼 작게 유지되는 이유입니다 — 그리고 이는 상위 어딘가에서 인증서를 생성해야 한다는 것을 의미합니다.

전체 기계어(machine-word) 도메인에 대한 의무를 다루려면 열거(enumeration)는 확장되지 않으며, 열거하지 않는 결정 절차(decision procedure)가 필요합니다: 재생 가능한 인증서를 방출하는 솔버 없는 제거(solver-free elimination). 그 엔진, 반박에서 최소 가드를 도출하는 수리 합성기(repair synthesiser), 그리고 그것들을 구동하는 진화 탐색(evolutionary search)은 이 저장소에 없으며 상업적으로 제공됩니다.

이 분할은 의도적이고 영구적입니다. 검증기는 무료이며 앞으로도 무료입니다 — 독립적으로 검증할 수 없는 인증서는 가치가 없으므로, 검증에 비용을 청구하면 형식의 목적을 무너뜨릴 것입니다. 비용이 드는 것은 대규모로 인증서를 생성하는 것입니다.

라이선스

클라이언트 및 툴 계층에 대해 Apache-2.0.

고속 경로(fast-path) 수치가 도출된 방법

위에서 인용한 속도 향상은 6.06x 중앙값, 3.55x–10.25x 관측 범위, 형태당 11회의 짝지은 반복입니다. 이 수치는 먼저 두 번 틀린 끝에 도달했으며, 그 기록은 여기 — 결과 아래, 수치를 감사하려는 독자가 찾을 수 있는 곳에, 수치 자체 앞이 아닌 곳에 보관됩니다.

• 철회됨 — 6.18x. 표본이 너무 작아 함께 인용된 범위를 뒷받침할 수 없었습니다.

• 2026-07-31 수정 — 2026-07-30 수정 자체가 근거가 없었습니다. 2026-07-30에 이전에 게시된 수치(1,698.7 ms -> 245.7 ms, 6.82x 중앙값 (범위 6.65-6.98x), 7회의 짝지은 반복)는 어떤 산출물에도 나타나지 않으며, 산술도 성립하지 않습니다: 1,698.7 / 245.7 = 6.91이며 6.82가 아닙니다. 인용된 범위는 또한 측정된 모든 형태보다 좁았습니다 — 폐기된 6.18x 수치가 이미 지니고 있던 것과 동일한 n-부족 오류입니다.

• 현재 수치는 make bench-fast-path(artifacts/crs/bench_fast_path.json)의 커밋된 출력입니다: 형태당 11회의 짝지은 반복, 모든 반복에서 비트 단위로 동일한 카운트, 그리고 그 하위 집합이 아닌 실제로 관측된 것에서 인용된 범위.

이를 통해 도달한 규칙: 이 저장소의 성능 주장은 커밋된 하네스로 재생성 가능해야 하며, 범위는 가장 좋은 몇 개가 아닌 측정값에서 나와야 합니다.

라이선스, 인용, 기여

Apache-2.0 (LICENSE). 게시하는 작업에서 이를 사용한다면, CITATION.cff에 기계 판독 가능한 인용 메타데이터가 있습니다 — GitHub의 "이 저장소 인용" 버튼이 이를 읽습니다.

• CONTRIBUTING.md — 팀 규칙과 변경이 깨뜨리지 말아야 할 하나의 불변 조건.

• ARCHITECTURE.md — 모듈 맵과 신뢰 경계(trust boundary)가 위치한 곳.

• TROUBLESHOOTING.md — 실제로 출력하는 오류 메시지에 맞춰 구성됨.

• SECURITY.md — 거짓된 것을 받아들이는 검증기는 여기서 가장 높은 심각도 등급입니다.

**인증된 발견(certified discovery)**의 일부 — 하나의 비대칭성 위에 구축된 10개의 산출물: 증명을 검증하는 것은 저렴하고 감사 가능하므로, 그것을 생성한 것은 신뢰할 필요가 없습니다.