The deterministic engine
Where a gate exists, the guarantee is absolute: an answer is returned only if an exact check accepts it (for bounds checks, a proof over *every possible buffer*, cross-checked against the Z3 solver on 1,500 random expressions), and a proven answer comes back identically, instantly, with no model call, forever after.
A model writes text by weighing probabilities, so the same question can get different answers, and any answer can be wrong. OwnLLM's deterministic engine (ownllm det) turns that around: the model is the last resort, not the engine. Answers come from proven knowledge and rules first. A model is asked only when nothing proven applies, and *nothing it says is used or remembered unless a proof gate accepts it.*
The cascade
Every question is a *hole* (a typed question for one kind of problem, called a vertical). It is offered to each tier in order of cost, and the first verified answer wins:
| Tier | What answers | Model? | Checked? |
|---|---|---|---|
| 0 Recall | an answer proven earlier, returned exactly as stored | no | re-checked by the gate on every recall |
| D Closed form | a rule the vertical already knows | no | proof gate |
| 1 Learned template | a rule inferred from two earlier proven answers | no | proof gate |
| M Model | a schema-constrained proposal from the local model | yes | proof gate, with retries |
| - Unresolved | nothing passed; queued for later | - | never guessed |
When the model's proposal fails the gate, the *reason* (a concrete counterexample where there is one) goes back into the next prompt. When it passes, the answer is crystallized: stored compressed on disk, and, when two proven answers share a pattern, folded into a reusable rule. So the model is needed less and less, and a repeated or structurally similar question returns instantly, identically, with no model call.
What is guaranteed
- Nothing is accepted without passing the vertical's gate, whichever tier produced it: rules and model alike.
- Same input, same answer. The rules are ordinary code; the model runs with no randomness (on the same computer and engine build); stored answers are returned byte for byte, and once an answer is stored the model is out of the picture.
- Recall is free: a proven answer costs no model call, ever again.
- Scope is enforced first: one person's stored answers are never served to, or merged with, anyone else's.
Where it applies
The guarantee is "this passed the gate", so it applies to the problem types that have a gate. Today:
| Vertical | The gate checks |
|---|---|
length-prefix-parsers | An exact proof that a bounds-checked read stays inside the buffer, lands inside the stated limit, and starts at the stated offset, for *every possible buffer*. Counterexamples come with concrete values. |
patent-claims | Every antecedent term appears in the claim text as whole words; the listed dependencies are exactly the claims the text refers to; the claim index is consistent with them; the classification code is well-formed. (The outline text is not checked.) Plus a separate claim linter (numbering, dependencies, antecedent basis). |
For free-form questions (chat, ask) there is no gate, so those answers are repeatable but not verified. Adding a vertical means writing its gate (det/src/verticals/); the cascade, lattice and model client need no changes.
Using it
ownllm det demo # watch it learn, with no model at all
ownllm det solve length-prefix-parsers '{"pre_buflen_min":6,"post_max":65535,"offset_hint":2}'
ownllm det submit length-prefix-parsers '<context json>' '<fill json>' # put any candidate through the gate
ownllm det lattice # what has been proven and stored (compressed)
ownllm det claims claims.txt # lint numbered patent claims
ownllm det arith --pre 2 --post 65535 '<expression json>'solve uses your local OwnLLM model as the last-resort tier when ownllm start is running.
Details worth knowing
- The bounds proof is exact, not estimated. Every read is an independent unknown that appears once, so the smallest and largest results come from interval arithmetic: a decision procedure. Our tests also put 1,500 random expressions to the Z3 solver and require agreement (
cargo test --features z3-check). Z3 is not needed to run it. - The claim linter is a rule-based reader of English: its antecedent-basis warnings can be wrong, and passing every check does not make a claim valid. It is not legal advice.
- The "novelty differential" field produced by the patent rules is an auto-generated outline, not an analysis.