# smt > Native bounded QF_LIA/QF_LRA decision operations. > Generated by `sema doc` from the compiler's authoritative native-signature registry. # smt (native adapter) Governed bounded QF_LIA/QF_LRA decision adapter — bring it in with `import smt`; calls require `proc.run`, checked counterexamples disprove, and external unsat remains unverified. # formal ## `smt.solve(claim, logic) -> SmtResult` Request a bounded external SMT decision. Exact counterexamples are independently replayed; unsat remains digest-bound unverified solver evidence and never becomes Proved. - domain: one UTF-8 equation-language claim up to 64 KiB in the bounded quantifier-free linear fragment and the exact literal theory QF_LIA or QF_LRA; at most 20,000 AST nodes, depth 256, 64 variables, 1 MiB script/output, 5 s solver soft timeout, and 31 s host deadline; the configured Z3 executable is resource-gated before version probing - shape: finite set / three-valued logic - returns: `SmtResult` - effects: `proc.run` - example: `smt.solve("\"x\" < \"y\" implies \"x\" + 1 <= \"y\"", "QF_LIA")` ## `smt.check(claim, logic) -> SmtResult` Produce and integrity-check replayable solver evidence. A checked counterexample disproves the claim; external unsat is explicitly unverified until an independent proof object exists. - domain: the same bounded QF_LIA/QF_LRA claim, solver, resource, size, variable, and timeout contract as smt.solve - shape: finite set / three-valued logic - returns: `SmtResult` - effects: `proc.run` - example: `smt.check("\"x\" < \"y\" implies \"x\" + 1 <= \"y\"", "QF_LRA")` ## `smt.prove(claim, logic) -> SmtResult` Produce an immutable sema.smt-proof/v1 object only after solver-independent exhaustive native replay. Proved results bind the canonical negated obligation, theory, kernel, atom set, assignment count, single-assertion unsat core, and proof reference. - domain: one UTF-8 equation-language QF_LIA/QF_LRA claim up to 64 KiB; exact linear normalization followed by exhaustive replay of at most 4,096 formula nodes and all valuations of at most 12 independent normalized atoms; returns typed Unknown outside this deliberately bounded proof calculus and never invokes an external solver - shape: finite set / three-valued logic - returns: `SmtResult` - example: `smt.prove("\"x\" < 0 or \"x\" >= 0", "QF_LRA")` ## `smt.verify(claim, proof) -> SmtResult` Replay a checked SMT proof against the caller-supplied claim and return a fresh immutable authenticated SmtResult. This API never trusts Z3 output, nominal type names, or a proof_ref without re-running the bounded native proof calculus. - domain: one UTF-8 equation-language claim up to 64 KiB plus an exact sema.smt-proof/v1 SmtProofObject; the proof-carried QF_LIA/QF_LRA theory, every identity field, canonical obligation, atom valuation, and native unsat core are re-derived; malformed objects fail typed and rejected proofs remain unaccepted - shape: scalar - returns: `SmtResult` - example: `smt.verify("\"x\" = \"x\"", smt.prove("\"x\" = \"x\"", "QF_LIA").proof_object)`