smt-contract-prover
SMT Contract & Policy Logic Prover — Answers a yes/no logic question about contract clauses, IAM/OPA policies or business rules with a solver-backed result and a plain-language headline and next step. Takes clauses or pasted text (or a formal IR directly with zero LLM calls), formalizes them into typed Boolean, integer and rational constraints, then answers "is P possible", "does invariant I always hold" or "are any clauses contradic
Tool call template
This tool declares no required parameters. Add optional parameters from the input schema as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {},
"name": "smt-contract-prover"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| ir | No | Formal IR, solved with zero LLM calls: {variables:[{name,type:bool|int|real,min?,max?}], constraints:[{id,expr,source?}], query:{mode:possible|always|consistency,formula?,source?}}. Expressions are JSON ASTs: {op:"var",name}, {op:"num",value:"3/4"}, {op:"true"|"false"}, and {op,args} for not, and, or, implies, iff, ite, =, !=, <, <=, >, >=, add, sub, neg, mul (one side constant). Numbers are exact strings. | |
| text | No | Alternative to clauses: the contract, policy or rules pasted as plain text. It is split into clauses by blank lines and numbered or bulleted lines (ids C1.2 or S3). Use clauses when you need your own ids. Requires query. | |
| query | No | The question, e.g. "Can an unauthorized user ever approve a payout over $10,000?" or "Are any clauses mutually contradictory?". Required with clauses. | |
| budget | No | Optional lower step budgets. | |
| clauses | No | Natural-language contract clauses, IAM/OPA policy statements or business rules, each with a caller-chosen id. Mutually exclusive with ir. |