verify
Checks whether an LTL assume-guarantee contract's assumptions and guarantees can hold together, returning a witness trace when satisfiable or conflicting core terms when unsatisfiable.
Instructions
Can the assumptions and the guarantees hold together (A & G
satisfiable, the verify command of logics_tool)? status is that of
feasible: sat with a witness trace, which also shows compatibility (A
satisfiable) and consistency (A -> G satisfiable); unsat when the
guarantees cannot hold when the assumptions do, and then compatible and
consistent say whether the assumptions alone cannot hold. With core, an
unsat result carries the terms that conflict (in feasible.core).
context: formulas that every behavior satisfies (e.g. an axiom of an
encoding, a physical law); the behaviors that violate them are left out.
Tool call template
Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {
"contract": "<contract>"
},
"name": "verify"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| core | No | ||
| backend | No | auto | |
| context | No | ||
| timeout | No | ||
| contract | Yes |