← back to the validity trial

Validity + Synthesa — capability & persona guide

Read this first. It tells each kind of user (and the host model driving the tools) how to get the best out of Validity + Synthesa through this MCP server. The server is also able to hand you this file as the resource validity://guide.

Validity turns the decidable decision domain — authz, policy, pricing, eligibility, safety, refund/return rules, approval flows, state machines, any "given these facts, what do we do" logic — into something you can prove, not just review. In the hosted service, your MCP host/model can author candidate specs and explain findings; the deterministic engine is the source of truth. compile_spec needs a separately registered drafting executable and returns an explicit unavailable result when none is configured.

The mental model (don't skip this)

For any decision spec, the engine classifies every input situation as one of three:

Three rules follow from this, and they govern how to use every tool:

1. The engine PROVES; an authoring model or human DRAFTS and EXPLAINS. Candidate YAML and prose are drafts. check_completeness / prove_conformance are the proof.
2. Model output is never evidence. When you explain gaps/contradictions to a human, say "the engine proved…" — never present your own phrasing as the guarantee. The signed receipt (attest_spec) is the evidence; it re-verifies offline with verify_receipt.
3. Green ≠ complete. A conforming implementation can still leave situations undefined. prove_conformance says "the impl matches the rules"; check_completeness says "the rules actually decide every case." Run both.

The 21 tools

THE flow (front-and-center): point Validity at rules you already run → import_seams on Go source (see the holes — cases your code decides wrong or not at all) → check_completeness / prove_conformance (prove the fix) → manufacture (get generated library source in your language) → integrate and test it → grade → attest_spec / residual (the receipt). Or start from proven: inspect with stdlib_list / stdlib_from, edit the returned specs, then call manufacture(..., base_stdlib_id: "<id>"). MCP reuses Core's new --from provenance and full build gate, so a weakened locked guard is refused before generation.

The classic hosted flow (author-first): author the strict intent/impl directly → check_completeness → prove_conformance → (resolve gaps, optionally bind_gaps) → attest_spec. Use compile_spec only when the deployment reports that a separate drafter is available.

Engine-authoritative, always. manufacture / grade / residual / import_seams / evolve_diff / audit_project each shell to a proving binary — model output is never the evidence. A tool that cannot prove its result fails closed (never a false COMPLETE / CORRECT / HONEST_BUILD). manufacture refuses to emit from an unproven table.

Connect to the hosted MCP correctly

The endpoint is https://validitymcp.byteverity.com/mcp. Every POST must send a bearer token, JSON content type, both Streamable-HTTP accept types, and the MCP protocol version:

curl -sS https://validitymcp.byteverity.com/mcp \
  -H "Authorization: Bearer $VALIDITY_TOKEN" \
  -H 'Content-Type: application/json' \
  -H 'Accept: application/json, text/event-stream' \
  -H 'MCP-Protocol-Version: 2025-06-18' \
  --data '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-06-18","capabilities":{},"clientInfo":{"name":"curl","version":"1"}}}'

Then send tools/list, read validity://guide, and call the needed tools with the same headers. A weekly trial grant meters admitted tools/call invocations only; initialization, discovery and resource reads are free but rate-limited. An admitted tool call consumes one unit even when the tool returns a domain error. Responses after a metered call include X-Trial-Quota-Limit, X-Trial-Quota-Remaining, and X-Trial-Quota-Reset.

Personas — how each gets the most out of it

1. Product Manager — "find the holes in my PRD before the sprint"

Want: the cases engineering will silently guess, and the requirements that contradict. Use: have your host model author the rule-shaped part as strict intent/impl YAML → check_completeness (or use compile_spec only when a drafter is registered). Read the result as: gaps = "you didn't say what happens when …" ; contradictions = "rule X and rule Y can't both hold for …". Turn each into an open question for the spec owner. Example: a refund policy with "Enterprise always gets a full refund" + "ToS violators are denied" → check_completeness proves the contradiction for an enterprise ToS-violator, and the gap for requests after the stated window. Decide them before building. Tip: keep inputs few and enumerable (bools/enums). Don't ask it to grade prose quality — it proves logic, not taste.

2. Program / Project Manager — "will the program integrate?"

Want: to catch cross-team interface breaks at the contract level, months before integration. Use: model each workstream as an atom (its own intent+impl) and each dependency as a seam (producer.output → consumer.input), then compose_system. Read the result as: composed:false with a named seam = "team B's component assumes a value team A's component never guarantees." Fix the contract, not the integration. Tip: start with the few load-bearing seams; you don't need to model the whole program.

3. Developer / SDET — "catch decision-logic bugs with a witness"

Want: proof the code matches the spec, and the exact input where it doesn't. Use: prove_conformance(intent, impl). Counterexamples are real failing inputs you can turn straight into a regression test. Pair with check_completeness to find untested gaps your tests would never have hit. Great for DMN / business-rule tables exported from Camunda/Drools/Excel. Tip: a NOT READY: invariant violation + counterexample is a forbidden-state breach — the highest-severity finding. Choosing between candidates? arbitrate(intent, [implA, implB, …]) runs every rival through the full pipeline and ranks them best-first — the winner, plus each loser's verdict and the exact counterexample that sank it. Use it to compare a refactor against the original, or two agent-written patches, before you prove and ship the winner.

4. Policy / Compliance author — "prove the rules are complete and hand an auditor proof"

Want: no fail-open hole in a regulated rule set, no internal contradiction, and a receipt a regulator can re-check. Use: check_completeness (no gaps/contradictions) → attest_spec (the sealed receipt). Hand the auditor: the receipt + the public key; they run verify_receipt air-gapped. "They have dashboards; you have proof." A forged "complete: true" does not survive the re-check. Tip: the receipt records which situations were checked and the regime — it's the exhaustive audit trail, not a summary.

5. AI / Agent builder — "gate the agent's action with a proof, recorded"

Want: an inline decision the agent's control layer can enforce, backed by a proof, with a receipt. Use: check_completeness returns a control route — accept (proven, proceed), ask (a gap; escalate to a human), revise (a contradiction; fix the policy), retrieve (need more evidence), refuse (a hard rule broken; block). Enforce the route at the action boundary; attest_spec gives the recordable proof. This is the basis of "block-with-a-proof, recorded." Tip: route ask/refuse are the safe defaults — never auto-accept on an unproven spec.

6. Auditor / Regulator / counterparty — "verify without trusting the vendor"

Want: to re-check a claim yourself, offline. Use: verify_receipt(receipt, public_key_hex). It uses only a public key — no engine, no solver, no network. verified:true with the recorded claims, or verified:false on any tamper.

7. Markets desk — trading & credit analyst — "find the case the contract forgot"

Want: the exact situation a contract, covenant, or market rule does not determine — the gap where a dispute, a loophole, or a loss lives — surfaced before the counterparty finds it. Use: paste the clause; your own model here compiles it into a decision table (few enum inputs = the situation, one output = what the clause decides — model only what it says, leave silent cases unruled), then check_completeness. Read the result as: a gap = "the clause is silent when …" (e.g. a PPA curtailment during negative prices that also coincides with a grid constraint — economic-and-compensable or grid-and-excused?; a take-or-pay shortfall caused by force majeure — excused or owed?; a bond covenant's pro-rata sharing amended via an undefined 'open market purchase' — the Serta uptier). A contradiction = two clauses collide. Then attest_spec for a signed receipt you can hand a desk head, an IC, or a counterparty. Example: the Serta 2016 covenant → check_completeness proves the exact (pro-rata, majority, open-market-purchase) cell is undetermined — the $1.3B loophole a court later held ambiguous. Same tool: a curtailment, a change-in-law/carbon-pass-through silence, an F&O ban threshold, a capacity-accreditation rule change. Tip: the completeness gap is necessary, not sufficient — pair it with the catalyst and the position. And it is honest both ways: a genuinely tight clause returns complete — the tool is not rigged to always cry "gap."

8. QA / Test engineer — "find the cases my tests miss, and the exact input that breaks"

Want: the untested situations your suite never reaches, and the concrete failing inputs — turned straight into test cases and regressions, without hand-guessing edge cases. Use: pull the decision under test out of your code into a small impl (the branch logic: a few enum/bool inputs → the outcome) and the requirement into intent (what it must always do / must never do). Then check_completeness (the gaps your tests would never hit) and prove_conformance (bugs, each with a witnessing input). Let your Claude do the extraction from a pasted function. Read the result as: each gap = an input situation your tests never covered → write one; each counterexample = a concrete input where the code disagrees with the spec → a ready regression test; a forbidden-state breach (NOT READY: invariant violation) = the highest-severity bug. Example: rule "never refund more than the remaining refundable balance" vs code that ignores already_refunded → prove_conformance returns the exact input that over-refunds (paste it as a failing test), and check_completeness flags the situations the logic left undecided. Fix, re-run, prove it's closed. Tip: this exhaustively covers the decision core — the risky branch logic, permission checks, pricing/eligibility, DMN/business-rule tables exported from Camunda/Drools/Excel — not your whole app. It doesn't replace integration or UI tests; it hands you the exact witnesses those tests would have taken luck to find. Pair with compose_system to catch a break at a module seam before integration. More you get here: (1) behavior-preservation on refactor — make the old behavior the intent and prove_conformance the new code: it proves the refactor changed nothing, or hands you the exact input where behavior drifted. (2) the gap cells ARE your missing-test matrix — one row per untested situation; bind_gaps even drafts the expected output for each, for the owner to confirm. (3) a signed QA sign-off — attest_spec turns "the decision core is exhaustively covered" into a receipt you attach to the PR/release, re-checkable offline: sign-off becomes an artifact, not a checkbox.

9. Security / Authorization engineer — "prove there's no fail-open access decision, and no conflicting grant/deny"

Want: no request the authorization policy leaves undecided (a default silently wins — the classic privilege-escalation / fail-open hole), and no two rules that both grant and deny the same request. Use: model the access decision — request attributes (role, resource, action, context flags) as enum/bool inputs, allow/deny as the output, each policy rule as an obligation — then check_completeness. This is the flagship decidable domain — the same shape as Cedar / Zelkova / OPA-Rego / firewall & IAM policy analysis, but ending in a signed receipt. Read the result as: a gap = an access request with no determined verdict; a contradiction = a rule collision (allow and deny both required). attest_spec → hand a security review or auditor proof the policy is total and consistent; prove_conformance → the enforcement code actually matches the policy. Example: "managers can approve" + "no one approves their own request" → check_completeness proves the manager-approving-their-own-request case is undetermined (which rule wins?), and flags any grant/deny conflict. Already have a Cedar policy? propose_from_policy(policy, world) drafts the checkable contract for you: give it the .cedar source + the finite world it's proven over (the enumerable principals / actions / resources / attributes), and it freezes today's decision frontier both ways — the deny-frontier as safety obligations (catch any future widening) and the allow-frontier as postconditions (catch any breaking). Review the draft, then check_completeness to see what the policy leaves undecided. The 3-minute answer to "did this innocent-looking policy diff quietly widen access?" Tip: also covers policy-as-config — OPA/Rego, IAM, security groups, network ACLs, feature-flag rollout gates. Prove the policy; free-form context (arbitrary strings) is reported, never faked.

10. Business-rules / decision-table owner (DMN) — "audit my rules table for gaps, conflicts, and redundancy"

Want: the person who owns a decision table — pricing, eligibility, routing, discounting, often in Camunda / Drools / Excel / DMN — wants it proven complete (a rule for every case) and consistent (no rows that fire different outcomes for the same facts) before it ships. No coding required. Use: the table is the impl (ordered when/then); the business requirements are the intent → check_completeness + prove_conformance. This is exactly the DMN gap / overlap / completeness analysis the decision-table literature formalizes — with a proof and a receipt instead of a linter's warning. Read the result as: a gap = a fact combination no row handles (the default wins, unnoticed); a contradiction = requirements that can't all hold. Example: a discount matrix where some region × tier × channel combination has no row → the default price applies silently; check_completeness names the exact combination. Tip: enum/bool columns enumerate exhaustively; a free-number column (an exact amount) is reported as a boundary, never faked. Ideal for tables exported from Camunda/Drools/Excel.

11. Underwriting / eligibility owner (insurance · benefits · healthcare) — "prove the rating/eligibility rules decide every case"

Want: an underwriter, actuary, or benefits / utilization-management owner wants the rating, eligibility, or coverage rules proven to decide every applicant or claim — no cliff, no silent gap, no contradiction — plus a receipt for the regulator. Use: model the applicant/claim facts (age band, plan, risk flags, thresholds) → the decision (eligible / rate tier / deny / prior-auth), each rule an obligation → check_completeness → attest_spec. Read the result as: a gap = a profile the rules don't decide (an adjuster guesses — an inconsistency, later an appeal); a contradiction = two eligibility rules collide. Example: a prior-auth policy where two clinical criteria interact so a sicker patient is denied while a healthier one qualifies → check_completeness surfaces the undetermined / contradictory cell before it becomes an appeal or a headline. Tip: the regulated-underwriting sweet spot (e.g. AIUC-1 quarterly re-testing) — the signed receipt is the re-test evidence, re-checkable offline.

12. CVE Exploitability / VEX Analyst — "prove which CVEs can actually hurt you, and emit a real VEX"

Want: kill scanner false positives with a proof — a defensible not_affected / affected verdict per CVE for your deployment, emitted as an OpenVEX / CSAF document the consumer re-verifies offline. Use: distil the advisory's exploit preconditions into finite facts (version-in-range, sink reachable, config flags, runtime, mitigation) and one obligation per advisory clause → check_completeness (an unpinned cell is the #1 false-positive source — the case the policy is silent on) → prove_conformance → attest_spec. Then emit_conforming(impl, facts, contract) renders the VEX deterministically — the trust artifact is code-made, never model-asserted; a new output format is a new contract (data), zero code. Read the result as: the completeness proof is your defensible VEX basis; not_affected becomes a receipt, not an assertion. Ships with this server: the vex-analyst persona (personas/vex-analyst.persona.md) and the proven disposition_to_vex mapping op (proofs/disposition_to_vex/, the format-agnostic fidelity table). Example: Spring4Shell present but no reachable POJO binding → check_completeness proves it, emit_conforming renders status: not_affected, justification: vulnerable_code_not_in_execute_path — with the receipt embedded.

13. Rules-owner / modernizer — "prove the rules I already run, then generate a proven replacement core"

Want: stop hand-porting a legacy rule table / policy engine and hoping it's right. Find the cases it decides wrong or not at all, fix them under proof, and ship the fixed decision into your stack — not as a report, as code. Use (the wedge, end-to-end): import_seams(source) on Go code you already run → it extracts each finite-decision seam, proves it, and names the holes (unhandled or contradictory cells — latent bugs). Resolve them (check_completeness / bind_gaps), then manufacture(intent, impl, lang) emits a proven decision function 1:1 into go / python / typescript / rust. Integrate and test that generated library source; grade it (non-circular), seal a residual / attest_spec receipt. Governing the change later: evolve_diff proves exactly which cells changed (nothing drifts undeclared); audit_project proves the build wasn't hand-tampered. Start-from-proven shortcut: inspect with stdlib_list → stdlib_from rbac_grant (or rate_admit / retry_decide / session_verdict / token_verify / transition_allowed), specialize the returned specs, then call manufacture with base_stdlib_id: "rbac_grant". The call preserves Core provenance, re-proves the variant and refuses a weakened locked guard before generation. The raw retrieval alone makes no such claim. Read the result as: the hole list is the bug report your proof wrote; the manufactured code is the fix, and the receipt is the evidence — checkable offline, in any language.

Write your own persona (a local .md your Claude reads alongside this guide)

None of the 13 fit your world exactly? Author your own — a short markdown file you keep locally and point your Claude at: "read my <domain>-persona.md and the validity guide, then check this: …". A good persona teaches your model your vocabulary, your decision shape, and what a gap means to you, so it drives the tools well instead of guessing. It composes with this guide — yours adds the domain, this one supplies the mechanics.

First, the litmus test — is your problem in scope? It fits if it's a decision over facts: "given these few facts, what do we do?", where the facts are enumerable (bools, enums, small integer bands) and the output is one decision from a small set. Authz, pricing, eligibility, approvals, refunds, covenants, routing, config guardrails — yes. Grading prose, ranking, scoring a continuous quantity, anything free-form or Turing-complete — no (the engine will say so, never fake it).

Then model it in five steps (the shape every persona above uses):

1. Name the decision — the one thing the rule outputs (allow/deny, eligible/deny/refer, a price tier, …).
2. List the facts that decide it — 3–6 bool/enum inputs. Resist continuous numbers; band them (age: <40, 40-64, 65+).
3. Write each rule as an obligation — "if C then output = D" (see Spec format below). Model only what the rule says; leave genuinely-silent cases unruled — that silence is exactly what check_completeness finds.
4. Translate the verdicts to your domain — a gap = "we never said what to do when …" (someone will guess); a contradiction = "these two rules can't both hold for …". Write that translation down; it's the heart of the persona.
5. Pick the flow — almost always check_completeness (gaps/contradictions) → prove_conformance if you also have code or a table to check → attest_spec when you want a receipt to hand someone.

Copy this template into your .md:

### <role> — "<the one sentence that names your pain>"
**Want:** <the exact undecided/contradictory case you're afraid of shipping>.
**Use:** model <your facts> as inputs and <your decision> as the output, each rule an obligation, then
`check_completeness` (+ `prove_conformance` if there's an impl/table, + `attest_spec` for a receipt).
**Read the result as:** a *gap* = <what "undetermined" means in your world>; a *contradiction* = <a rule
collision in your terms>.
**Example:** <one concrete facts→decision case, and the cell you expect to come back undetermined>.
**Tip:** keep inputs few and enumerable; model only what the rule states; the receipt is the audit trail.

Two rules that make a persona work:

• Keep it honest about the boundary. The engine proves the logic, not the taste. If your persona asks it to judge quality, tone, or an unbounded quantity, that part is out of scope — say so in the file so your model doesn't overreach.
• Never let the model's phrasing be the guarantee. Tell your Claude to attribute findings to the engine ("the oracle proved …") and hand the open questions to a human. The signed receipt is the evidence; your explanation is not.

Spec format (author intent + impl directly — no compile_spec needed)

A spec is two small YAML documents. The host model can write these reliably.

# intent.yaml — the rules / promises, as obligations
schema: validity.intent.v1
id: refund_policy
version: 1
inputs:
  - {name: within_window, type: bool}
  - {name: plan, type: enum, values: [monthly, annual, enterprise]}
  - {name: tos_violation, type: bool}
outputs:
  - {name: decision, default: deny}        # deny | full | prorated | approval_required
postconditions:
  - id: enterprise_always_full
    statement: Enterprise customers always get a full refund.
    predicate:
      any:                                  # "if plan==enterprise then decision==full"
        - {left: {var: in.plan}, op: ne, right: {const: enterprise}}
        - {left: {var: out.decision}, op: eq, right: {const: full}}
  - id: tos_violation_denies
    statement: A ToS violation denies the refund.
    predicate:
      any:
        - {left: {var: in.tos_violation}, op: eq, right: {const: false}}
        - {left: {var: out.decision}, op: eq, right: {const: deny}}

# impl.yaml — the ordered when/then decision table under test (last match wins; default covers the rest)
schema: validity.impl.v1
id: refund_policy.impl
intent: refund_policy
outputs:
  - {name: decision, default: deny}
rules:
  - id: r_enterprise
    when:  [{left: {var: in.plan}, op: eq, right: {const: enterprise}}]
    then:  [{set: out.decision, to: {const: full}}]

• Inputs: type: bool | type: enum, values: [...] | type: number, min, max, integer: true.
• Operators: eq ne lt le gt ge. Combinators: any:[…] (OR), all:[…] (AND).
• A rule "if C then D" is the obligation any: [ <C negated>…, {out.X == D} ].
• Keep the input space enumerable (bools/enums/small integer grids). The engine proves exhaustively over the declared domain; an unbounded number/string is reported, never faked.

Latest & greatest

• Exhaustiveness receipts (attest_spec) — in-toto/DSSE, offline-verifiable, with the control route folded in; bound to the spec identity so two different specs never collide.
• Control routes — the proof projected to accept / retrieve / ask / revise / refuse, the vocabulary an inline guardrail enforces and a flight-recorder captures.
• Assume-guarantee composition (compose_system) — prove a program-of-parts, not a monolith; it names the exact broken seam.
• Synthesa bind loop (bind_gaps) — close gaps from the spec's own decisions, each clause re-certified by the oracle; contradictions are surfaced for a human, never auto-resolved.
• Manufacture to executable source (manufacture) — a proven table becomes generated library source in go / python / typescript / rust, 1:1 from the proof. Integrating, compiling and testing it in the consumer repository remain explicit downstream steps.
• Trustworthy 3-way grade (grade) — CORRECT only when a fail-closed baseline fails, an independent gold and the candidate pass, and the check is decoupled. A vacuous or coupled passing test is not CORRECT — non-circular by construction.
• Signed residual (residual) — COMPLETE only when the residual is empty and every grade is trustworthy; a deterministic content root that recomputes offline. Never a false COMPLETE.
• Guard-locked stdlib (stdlib_list / stdlib_from) — inspect primitives and their declared guards, then pass base_stdlib_id to manufacture. The MCP path reuses Core's new --from provenance and full build gate; a weakened base guard is refused before code generation.
• Lifecycle — import_seams (find the holes in Go code you already run), evolve_diff (exhaustive behavioral diff + drift verdict), audit_project (the honest-build meta-check). Adoption → change management → integrity, all engine-authoritative.

Honest limits

• It proves the decidable part: rule-based decisions over enumerable inputs. It does not judge free-form text, ML model internals, or anything Turing-complete.
• An unbounded input (a free number continuum / string) means the spec can't be 100% complete; the engine says so (fail-closed) — it never reports a false "complete."
• compile_spec requires a separately registered drafting executable; the hosted deployment does not provide one today. The host model can author YAML directly. bind_gaps is different: it deterministically derives a proposed outcome from the supplied implementation for each gap, re-checks the result, and leaves every proposed clause for a human to confirm.
• import_seams currently accepts Go source only. manufacture emits generated library source; it does not modify, wire, compile or integration-test your consumer repository.

For the host model driving these tools

1. Prefer authoring intent/impl directly. Use compile_spec only if the deployment reports a registered drafter; then always check_completeness before claiming anything.
2. When you report gaps/contradictions/counterexamples, attribute them to the engine ("the oracle proved…") and present the open questions for a human — don't assert your explanation as the guarantee.
3. End a review with attest_spec when the user wants something durable/auditable, and tell them it re-verifies offline with verify_receipt.
4. Respect the route: ask/revise/refuse mean don't proceed — surface them, don't paper over.