Axiomatic agents · Lean4 + LLM predicates
⌜
⌟
A toolkit of agents that wrap a Lean4 kernel around LLM-backed predicate functions. Predicates return Booleans with evidence. The kernel composes the proof. Two products, one method, two domains.
Qnarre
verifier
legal complaints, checked against encoded statutes
statutes civil RICO · Title VI · §§ 1981/1983/1985
evidence every element, quoted and cited
trace Lean kernel, lake-built, exportable
illustrative · synthetic complaint (Doe v. Acme)
00:00 culpable-person → true
07:13 is-enterprise → true
14:26 engaged-in-interstate-commerce → true
21:39 employed-or-associated → true
28:52 conducts-or-participates → true
35:05 racketeering-activity → true
42:18 racketeering-activity → true
49:31 within-ten-years → true
56:44 related → true
03:57 continuous → true
10:10 person-enterprise-distinct → false
17:23 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise
24:36 culpable-person → true
31:49 is-enterprise → true
38:02 engaged-in-interstate-commerce → true
45:15 employed-or-associated → true
52:28 conducts-or-participates → true
59:41 racketeering-activity → true
06:54 racketeering-activity → true
13:07 within-ten-years → true
20:20 related → true
27:33 continuous → true
34:46 person-enterprise-distinct → false
41:59 ⟶ §1962(c): one element unmet — VALID requires person ≠ enterprise
Open Qnarre →
Qresev
evaluator
stocks and portfolios, axiomatically evaluated
frameworks trend · momentum · sector · drawdown
options defined-risk only — strictly enforced
evidence OHLCV + indicators, quoted to the bar
00:00 sma-50 > sma-200 → true
07:13 macd-bullish-cross → true
14:26 rsi-14 in [30,70] → true
21:39 r-squared(slope, 1y) → 0.71
28:52 atr-14 < 1.5σ → true
35:05 sector-cap(Tech) ≤ 30% → false
42:18 defined-risk-only → true
49:31 covered-call-collateral → true
56:44 protective-put-bound → true
03:57 drawdown-90d ≤ 12% → true
10:10 gics-concentration ≤ cap → true
17:23 volume-confirmation → true
24:36 momentum-percentile ≥ 70 → true
31:49 volatility-regime stable → true
38:02 sma-50 > sma-200 → true
45:15 macd-bullish-cross → true
52:28 rsi-14 in [30,70] → true
59:41 r-squared(slope, 1y) → 0.71
06:54 atr-14 < 1.5σ → true
13:07 sector-cap(Tech) ≤ 30% → false
20:20 defined-risk-only → true
27:33 covered-call-collateral → true
34:46 protective-put-bound → true
41:59 drawdown-90d ≤ 12% → true
48:12 gics-concentration ≤ cap → true
55:25 volume-confirmation → true
02:38 momentum-percentile ≥ 70 → true
09:51 volatility-regime stable → true
Open Qresev →
Sample trace · one run, three stages loop 5.0s
PARSEPREDICATEELABORATE
The natural language of a complaint or a portfolio is a noisy carrier of structured facts. We make the carrier explicit. A predicate is a function from evidence to Boolean. The kernel is a referee that has read the rules and refuses to be persuaded. That is a narrower claim than it sounds — and the right one: not that the conclusion is true, but that the disagreement is auditable.
Read the full thesis →Public artifacts