minicheck-mcp

MCP 서버로 동작하는 모델 체커. 에이전트가 추측하는 대신 상태 머신을 검증하게 하세요.

왜 이런 것이 필요한가

에이전트는 끊임없이 상태 머신을 설계합니다 — 재시도 루프, 잠금 프로토콜, 세션 수명 주기, 하위 에이전트 간 핸드오프 — 그리고 나서 정확성을 산문으로 추론합니다. 동시성에 대한 산문 추론은 모델에게도 사람과 똑같이 실패합니다: 떠오르는 인터리빙만 고려하고 떠오르지 않는 하나를 놓치는 방식으로요.

결정 절차를 가진 에이전트는 추측할 필요가 없습니다. 판정을 받고, 속성이 실패할 때는 그것을 깨뜨리는 정확한 단계 시퀀스를 받습니다 — 그것은 설계를 사과하는 대신 고치는 데 필요한 것이기도 합니다.

보내는 스펙은 데이터이지 코드가 아니므로, 에이전트가 제출한 어떤 것도 실행되지 않습니다 — 그리고 돌아오는 것은 최단 반례 추적이 포함된 판정입니다.

Related MCP server: agent-gate

설치

# from GitHub (PyPI release pending)
pip install "minicheck-mcp @ git+https://github.com/nickharris808/minicheck-mcp.git"
pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git"  # + the MCP SDK

pip install minicheck-mcp는 아직 작동하지 않습니다 — 패키지가 PyPI에 없습니다. 위와 같이 GitHub에서 설치하세요; 그러면 minicheck이 자동으로 함께 설치됩니다. python build_pypi.py는 두 패키지가 모두 게시될 때 PyPI에 업로드 가능한 아티팩트를 생성합니다 (PyPI는 이 패키지가 인덱스 없이 설치 가능하도록 사용하는 직접 의존성 참조를 거부합니다).

그런 다음 등록하세요 (claude_desktop_config.json 또는 아무 MCP 클라이언트):

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

저장소는 이것을 mcp.json으로 제공합니다.

30초 퀵스타트

에이전트에게 물어보세요: "성공할 때까지 카운터를 증가시키는 재시도 루프가 있습니다. 3번 이상 재시도할 수 없는지 확인해 주세요." 그러면 에이전트는 이 스펙을 check_invariant로 보냅니다:

{
  "name": "retry",
  "fields": ["tries", "done"],
  "initial": {"tries": 0, "done": 0},
  "transitions": [
    {"label": "attempt", "when": {"done": 0}, "set": {"tries": {"incr": 1}}},
    {"label": "succeed", "when": {"done": 0}, "set": {"done": 1}}
  ],
  "invariants": {"bounded_retries": {"forbid": {"tries": 4}}}
}

그리고 돌아오는 것은 — 다음으로 재현하세요 python -c "from minicheck_mcp import dispatch; import json; print(json.dumps(dispatch('check_invariant', {'spec': SPEC}), indent=2))":

{
  "ok": true,
  "reachable_states": 129,
  "exhaustive": false,
  "invariants": {
    "bounded_retries": {
      "holds": false,
      "counterexample": [
        {"label": null,      "state": {"tries": 0, "done": 0}},
        {"label": "attempt", "state": {"tries": 1, "done": 0}},
        {"label": "attempt", "state": {"tries": 2, "done": 0}},
        {"label": "attempt", "state": {"tries": 3, "done": 0}},
        {"label": "attempt", "state": {"tries": 4, "done": 0}}
      ],
      "steps": 4
    }
  },
  "incomplete_reason": "IntBoundExceeded: transition 'attempt' drives field 'tries' to 65, outside int_bound 64. The state space is not finite under this bound, so no exhaustive verdict is available. Re-run with int_bound >= 65.",
  "advice": "the state space was not fully explored, so any invariant not refuted below is UNDETERMINED (null), not proved. Raise int_bound or add a 'when' guard that bounds the growing field, then check again.",
  "all_hold": false,
  "verdict": "REFUTED",
  "verdict_means": "a counterexample was found; it starts at the initial state and replays"
}

"이것은 영원히 루프할 수도 있습니다"가 아니라, 그것을 깨뜨리는 정확한 네 단계입니다.

하지만 전체 답변을 읽어보면, 이 퀵스타트가 바로 그 이유입니다: exhaustive는 false입니다. 반박은 그 자체로 유효합니다 — 반례는 자신의 증인을 지니고 그 추적은 재생됩니다 — 그러나 이 스펙의 다른 어떤 것도 확립되지 않았습니다. 왜냐하면 attempt에는 가드가 없고 tries를 int_bound 너머로 밀어내기 때문입니다. 반박에는 증인 하나면 충분하지만, 증명에는 전체 공간이 필요합니다.

튜토리얼 — 실제 세션이 어떻게 보이는지

에이전트가 세션 수명 주기를 작성했고, 세션이 닫힌 후에 사용될 수 있는지 알고 싶어 합니다. 전체 교환은 다음과 같습니다.

1. 에이전트가 형식을 요청합니다 (spec_help), 그런 다음 check_invariant를 보냅니다:

{
  "name": "session",
  "fields": ["state", "used"],
  "initial": {"state": 0, "used": 0},
  "transitions": [
    {"label": "open",  "when": {"state": 0}, "set": {"state": 1}},
    {"label": "use",   "when": {"state": 1}, "set": {"used": 1}},
    {"label": "close", "when": {"state": 1}, "set": {"state": 2}},
    {"label": "reopen","when": {"state": 2}, "set": {"state": 1}}
  ],
  "invariants": {"no_use_after_close": {"forbid": {"state": 2, "used": 1}}}
}

2. 정확한 경로가 포함된 반박을 받습니다:

{
  "ok": true,
  "verdict": "REFUTED",
  "exhaustive": true,
  "reachable_states": 5,
  "all_hold": false,
  "invariants": {
    "no_use_after_close": {
      "holds": false,
      "steps": 3,
      "counterexample": [
        {"label": null,    "state": {"state": 0, "used": 0}},
        {"label": "open",  "state": {"state": 1, "used": 0}},
        {"label": "use",   "state": {"state": 1, "used": 1}},
        {"label": "close", "state": {"state": 2, "used": 1}}
      ]
    }
  }
}

작성된 그대로의 불변식은 닫힌 세션을 사용한 적이 있는 것을 금지하는데, 이는 에이전트가 의도한 바가 아닙니다 — "닫힌 동안 use 전환 없음"을 의미했습니다. 반례는 그 차이를 그럴듯해 보이는 문단에 맡기는 대신 구체적으로 만듭니다.

3. 에이전트는 모델을 수정하고 다시 실행합니다. used는 "이 세션이 열린 이후 사용됨"을 의미해야 하므로, close가 그것을 지웁니다:

{"label": "close", "when": {"state": 1}, "set": {"state": 2, "used": 0}}

{"ok": true, "verdict": "PROVED", "exhaustive": true, "reachable_states": 4, "all_hold": true}

PROVED 그리고 exhaustive: true가 함께 읽어야 할 쌍입니다. 첫 번째는 두 번째 없이는 발급될 수 없지만, 둘 다 확인하는 것이 습관을 명시적으로 만듭니다 — 그리고 그 습관이 스펙이 한계를 넘어 성장하는 날 당신을 보호합니다.

4. 에이전트가 해서는 안 되는 일. 응답이 "verdict": "UNDETERMINED"라면, 그것은 통과가 아닙니다. 검색이 일찍 중단되었음을 의미합니다 — incomplete_reason과 advice를 읽고, 증가하는 필드를 제한하고, 다시 요청하세요. ok가 false이면 판정 자체가 존재하지 않으며 all_hold는 null입니다.

도구

스펙 형식

{
  "name": "mutex",
  "fields": ["a", "b", "lock"],
  "initial": {"a": 0, "b": 0, "lock": 0},
  "transitions": [
    {"label": "a_enter", "when": {"a": 0, "lock": 0}, "set": {"a": 1, "lock": 1}},
    {"label": "a_exit",  "when": {"a": 1},            "set": {"a": 0, "lock": 0}}
  ],
  "invariants": {"not_both": {"forbid": {"a": 1, "b": 1}}},
  "goal": {"require": {"a": 1}}
}

when은 field == value 테스트의 논리곱입니다 (항상 활성화하려면 생략). set은 리터럴을 할당하거나, 정수의 경우 {"incr": n} / {"decr": n}을 할당합니다. 불변식은 {"forbid": {...}} (나열된 모든 필드가 일치하면 실패) 또는 {"require": {...}} (일치하지 않으면 실패)입니다.

정수는 제한되어 있고, 그 제한이 검사됩니다 — int_bound (기본값 64)는 필드가 가질 수 있는 최대 크기입니다. 필드를 그 너머로 운반하는 실행은 값을 포화시키는 대신 중단되고 exhaustive: false를 보고합니다. 왜냐하면 조용히 잘린 검색은 방문하지 않은 상태에 대해 "유지됨"을 보고하기 때문입니다. 결과 판정을 읽는 방법은 정직한 범위를 참조하세요.

왜 선언적인가

에이전트가 제공한 Python을 exec하는 MCP 서버는 단계만 추가된 원격 코드 실행 구멍이 될 것입니다. 여기서 스펙은 데이터입니다: __import__('os').system(...)처럼 보이는 필드 값은 문자열로 남아 문자열로 비교됩니다. 정확히 그런 것을 주장하는 테스트가 있습니다.

SDK 없이도 사용 가능

도구는 일반 함수입니다. dispatch는 전송 계층이 사용하는 것과 동일한 진입점이므로, 에이전트 없이 스크립트나 테스트에서 호출할 수 있습니다:

from minicheck_mcp import dispatch
dispatch("check_invariant", {"spec": my_spec})

mcp가 설치되지 않은 경우, minicheck-mcp는 traceback을 내는 대신 설치 방법을 설명하는 JSON 오류를 출력하고 0이 아닌 종료 코드로 종료합니다.

정직한 범위

판정을 삼값으로 읽으세요. 이것이 에이전트에게 가장 중요한 부분입니다. 에이전트는 필드를 읽고 그것에 따라 행동하지, 문단에 판단을 가져오지 않기 때문입니다.

모든 응답은 또한 verdict_means를 포함합니다. 에이전트가 사용자에게 의역(그리고 어쩌면 순화)하는 대신 그대로 인용할 수 있는 한 줄 설명입니다.

모든 응답은 오류를 포함하여 all_hold와 holds를 명시적으로 포함합니다. 이전 버전은 실패 시 그것들을 생략하여, result.get("all_hold")가 충돌과 진짜 미결정 결과 모두에 대해 None을 반환했습니다 — 그리고 둘 다 거짓으로 취급되어 반박과 정확히 같았습니다.

exhaustive가 false일 때, 응답은 또한 무엇을 변경해야 하는지 지목하는 incomplete_reason과 advice를 포함합니다. 불변식이 자명하게 충족될 때 warnings 배열이 나타납니다 — 그것은 실제로 유지되지만, 아무것도 검증하지 않습니다.

무엇을 증명하는가. 유한한 선언적 상태 머신이 선언된 경계 내에서 모든 인터리빙에 대해 불변식을 만족하는지 여부.

무엇을 증명하지 않는가.

• 당신의 구현에 대해서는 아무것도 아닙니다 — 보낸 스펙에 대해서만. 스펙은 추상화입니다.

• int_bound (기본값 64) 또는 200,000 상태 상한 밖의 어떤 것도 아닙니다. 둘 중 하나를 초과하면 UNDETERMINED가 되며, 조용한 통과는 결코 없습니다.

• AG-EF를 넘어선 라이브니스에 대해서는 아무것도, LTL에서는 아무것도 아닙니다.

스펙의 어떤 것도 실행되지 않습니다. 스펙은 데이터입니다: 필드 이름, 리터럴, 비교. eval도, exec도, 스펙의 문자열을 호출 가능한 것으로 바꾸는 코드 경로도 없습니다. 그렇기 때문에 Python을 받아들이는 대신 선언적 로더가 존재합니다.

여기에 없는 것

이것은 엔진과 그것을 안전하게 호출하는 방법입니다. 유지 관리되는 위험 속성 말뭉치, 두 구성 요소가 결합될 때만 존재하는 위험을 찾는 구성 분석, 그리고 판정을 나중에 감사 가능하게 만드는 증거 추적은 상용 제품입니다. 이 서버는 MIT이며 그대로 유지됩니다.

문제 해결

ok: false, error: "SpecError". 스펙이 잘못되었고 메시지가 키를 지목합니다. 먼저 validate_spec를 호출하거나, 작업 예제가 있는 형식은 spec_help를 호출하세요.

통과할 것으로 예상한 스펙에서 verdict: "UNDETERMINED". 검색이 전체 상태 공간을 덮지 못했습니다 — 일반적으로 무한정 성장하는 필드 때문입니다. incomplete_reason과 advice를 읽으세요. 성장을 멈추는 when 가드를 추가하세요. 이것을 통과로 취급하지 마세요.

ok: false, error: "BadArguments". 도구가 받지 않는 인수로 호출되었습니다. 모든 도구는 spec을 받습니다; check_invariant는 선택적 invariant 이름도 받습니다.

check_liveness에서 "spec declares no 'goal'"과 함께 ok: false. 라이브니스는 도달할 무언가가 필요합니다. 불변식과 같은 모양의 goal 블록을 추가하세요.

warnings 배열이 나타났는데 불변식이 여전히 holds: true라고 말합니다. 불변식이 제한된 공간이 표현할 수 없는 값을 지목하므로, 프로토콜과 무관한 이유로 만족됩니다 — 일반적으로 리터럴의 오타 또는 금지하려는 값보다 낮은 int_bound입니다.

서버가 JSON 오류와 함께 즉시 종료됩니다. MCP SDK가 설치되지 않았습니다: pip install "minicheck-mcp[mcp] @ git+https://github.com/nickharris808/minicheck-mcp.git". 도구는 from minicheck_mcp import dispatch를 통해 SDK 없이도 import하고 테스트할 수 있습니다.

내 에이전트가 오류를 "속성은 괜찮다"로 취급합니다. 그럴 수 없어야 합니다: 모든 응답은 all_hold와 holds를 명시적으로 포함하며, 어떤 오류에서도 둘 다 null이고 verdict: "ERROR"입니다. 먼저 result["ok"]로 분기하세요.

성능

기본 체커에 의해 제한됩니다. 스펙은 여기 선언적으로 도착하며, 이는 체커의 컴파일된 경로입니다 — M-시리즈 노트북의 CPython 3.11에서 대략 초당 2.5×10⁵–7.5×10⁵ 상태이며, minicheck 저장소에서 python bench.py를 실행하여 재현할 수 있습니다. 수만 상태에 맞는 스펙은 1초 미만으로 응답합니다. 서버 계층 자체에는 측정된 병목이 없습니다 — 그것은 얇은 디스패치입니다.

FAQ

"언어 모델에서 스펙을 실행하면 코드가 실행되는 것 아닌가요?" 아닙니다. 그래서 선언적 형식이 존재하는 것입니다. 스펙은 데이터입니다: 필드 이름, 리터럴, 그리고 동등성 비교. eval도, exec도 없으며, 스펙의 문자열을 호출 가능한 것으로 바꾸는 코드 경로도 없습니다. __import__('os').system(...)처럼 보이는 필드 값은 문자열로 남아 문자열로 비교됩니다. 정확히 그 점을 단언하는 테스트가 있고, 적대적 테스트 스위트는 모든 도구에 코드 형태의 페이로드를 쏘아 넣습니다. (minicheck의 Python Model API는 다릅니다 — 그것은 코드이며, 거기서 나온 신뢰할 수 없는 모델은 신뢰할 수 없는 Python이 받아야 할 주의를 기울일 가치가 있습니다. 이 서버는 그것을 노출하지 않습니다.)

"그냥 에이전트가 Python을 작성하고 실행하게 하면 안 되나요?" 에이전트가 제공한 Python을 exec하는 MCP 서버는 단계만 추가된 원격 코드 실행 구멍일 뿐입니다. 선언적 형식은 표현력을 희생하는 대신 한 문장으로 말할 수 있고 테스트할 수 있는 속성을 얻습니다.

"제 에이전트가 all_hold를 읽고 속성이 괜찮다고 결론 내렸는데, 오류가 있었습니다." 그럴 수 없어야 합니다: 모든 응답은 all_hold와 holds를 명시적으로 담고 있으며, 오류가 발생하면 둘 다 null이고, verdict: "ERROR"와 ok: false가 함께 옵니다. 이전 버전은 실패 시 그것들을 생략했기 때문에, result.get("all_hold")는 크래시와 진짜 미결정 결과 모두에 대해 None을 반환했고 — 둘 다 거짓으로 취급되어 반박과 똑같았습니다. 먼저 result["ok"]로 분기하고, 그 다음 verdict로 분기하세요. 절대 all_hold의 진릿값으로 분기하지 마세요.

"왜 모든 응답에 verdict_means 문자열이 있나요?" 에이전트가 평결을 바꿔 말하면 그것을 순화시키는 경향이 있고, "검사가 결정적이지 않았다"는 두 단계만 거치면 "괜찮아 보인다"가 됩니다. verdict_means는 에이전트가 사용자에게 그대로 인용할 수 있는 한 줄 설명입니다.

"UNDETERMINED — 에이전트가 재시도해야 하나요, 아니면 성공으로 보고해야 하나요?" 기본적으로 둘 다 아닙니다. 검색이 일찍 중단되었음을 의미하므로 아무것도 확립되지 않았습니다. incomplete_reason과 advice를 읽으세요. 무엇을 바꿔야 하는지 — 보통 무한히 커지는 필드 — 를 알려줍니다. 그것을 제한하고 다시 요청하세요. 통과로 보고하는 것은 이 전체 패키지가 막아내려고 만들어진 실패 모드입니다.

"MCP SDK가 필요한가요?" 전송 계층으로 서빙할 때만 필요합니다. 도구는 평범한 함수입니다: from minicheck_mcp import dispatch는 전송 계층이 사용하는 것과 동일한 진입점이므로, 에이전트 없이 스크립트나 테스트에서 호출할 수 있습니다. mcp가 설치되지 않은 상태에서 minicheck-mcp 명령은 traceback을 내는 대신 설치 방법을 알려주는 JSON 오류를 출력하고 0이 아닌 종료 코드로 끝납니다.

"프로덕션 준비가 되었나요?" 네, 그리고 완전히 테스트되었습니다 — 하지만 주변 에이전트 생태계는 빠르게 움직이므로, MCP 표면이 버전 업데이트가 가장 필요할 부분입니다. 그 아래의 검사기는 minicheck이며 안정적입니다.

"여기서 뭔가가 저에게 확신을 주는 답변을 줬는데 틀렸습니다." 우회 방법보다는 이슈로 올릴 가치가 있습니다; 스펙을 포함해 주세요. 에이전트 직면 서버에서 도달 가능한 거짓 holds: true는 이 패키지가 가질 수 있는 가장 심각한 버그이며, 정확히 그런 종류의 버그 하나가 minicheck 0.1.0에서 발견되어 수정되고 공개되었습니다.

테스트

pip install -e ".[test]" && pytest

$ pytest -q
........................................................................ [ 74%]
.........................                                                [100%]
100 passed in 2.31s

102개의 테스트, 모든 도구가 실제 dispatch 경로를 통해, 잘못된 입력, 알 수 없는 도구, 코드 미실행 보장을 포함합니다. 하나는 이 README의 자체 테스트 수를 pytest --collect-only와 대조하여 단언하므로 배지가 어긋날 수 없습니다.

포트폴리오

하나의 아이디어가 모두를 관통합니다: 확인할 수 없는 평결은 평결이 아니다 — 그리고 여기의 모든 표면을 지배하는 그 귀결: 미결정은 통과가 아니다.

브라우저에서 사용해 보기 · 상태 머신 모델 검사 · specforge 리더보드

정답 데이터 · protocol-bench · specforge

상용 제공

이것들이 엔진입니다. 오픈 소스가 아닌 것은 규모에서 유용하게 만드는 것들입니다: 유지 관리되는 위험 속성 말뭉치, 두 구성 요소가 결합될 때만 존재하는 위험을 찾는 구성 분석, 신뢰 모델 민감도 스윕, 그리고 사후에 평결을 감사 가능하게 만드는 증거 추적. 위의 도구들은 MIT이며 그 상태를 유지합니다.

문서

개념 가이드와 TLA+, SPIN, Alloy, CBMC에 대한 정직한 비교를 포함한 전체 문서는 https://nickharris808.github.io/verification-docs/ 에 있습니다.

기여

버그 보고와 풀 리퀘스트를 환영합니다 — CONTRIBUTING.md를 참조하세요. 이 도구가 틀리는 반례는 보내실 수 있는 가장 유용한 것입니다.

인용

인용 메타데이터는 CITATION.cff에 있습니다; GitHub는 그것으로 Cite this repository 버튼을 렌더링합니다.

라이선스

MIT. LICENSE를 참조하세요.