FOL-LAB // MILESTONE 01 // 2026.09.01–04 // OLARES ONE

THE SOLVER DECIDES. THE MODEL TRANSLATES.

Formal Methods + Local AI. Making decisions auditable, testable, and deterministic. The LLM translates; independent SMT solvers decide.

← BEFORE FreeToken Z3 5.1.0 CVC5 1.3.4 LLM QWEN3-CODER 30B M1 COMPLETE NEXT → AI Regulation NEXT → revolut.hot

MISSION · M1 COMPLETE

BUILD A HYBRID SYSTEM WHERE A LOCAL LLM TRANSLATES NL → FORMAL SPECS — WHILE INDEPENDENT SMT SOLVERS MAKE DETERMINISTIC LOGICAL DECISIONS.

Core philosophy: move the LLM out of the position of final logical authority. The solver decides SAT/UNSAT; the LLM only translates and explains.

Architecture — seven stations

NL → DECISION → EXPLANATION

Natural Language Policy

Human-readable rules.

Qwen3-Coder 30B

NL → structured JSON.

JSON Schema Validation

Pydantic / deterministic check.

Mutation Testing

Boundary condition verification.

Z3 + CVC5 Solvers

Independent SAT/UNSAT evaluation.

Result Comparison

Agreement check.

Qwen Explanation

Formal result → plain English.

∅

Final authority

Never the LLM. Always the solver + validation chain.

Toolchain — all tools verified

OLARES ONE · HOME LAB

Z3 5.1.0

Microsoft SMT solver

Python API.

CVC5 1.3.4

Independent SMT solver

Python API. Second opinion by design.

SWI-Prolog 9.0.4

Logic programming engine

FOL layer.

Soufflé 2.5

Datalog engine

Provenance.

Clingo 5.8.2

Answer set programming

Rule exploration.

Lean 4.33.1

Theorem prover

Lake build.

Milestone 1 — results

THREE CASES · DUAL-SOLVER

▚ CASE A — ALLOWED DEMONSTRATED

Alice is KYC verified. Bob is not sanctioned. Transfer $8,000. Policy: transfers over $10,000 require review.

SAT

CVC5

SAT

DECISION

ALLOW

▚ CASE B — BLOCKED DEMONSTRATED

Transfer $12,000. Policy: transfers over $10,000 require enhanced review. Enhanced review NOT completed.

UNSAT

CVC5

UNSAT

DECISION

BLOCK

▚ CASE C — CONTRADICTION DEMONSTRATED

Policy A: block all transfers above $10K. Policy B: KYC-verified customers can transfer any amount. Alice is KYC-verified. Transfer $15,000.

UNSAT

CVC5

UNSAT

RESULT

CONTRADICTION

Proven vs not proven

READ BEFORE SHARING

DEMONSTRATED · M1

Local LLM produces machine-validated structured formalizations.
Two independent SMT solvers evaluate deterministic encodings.
Both solvers agree on SAT/UNSAT outcomes.
Contradictions are exposed explicitly, not hidden.
The LLM is removed from final logical authority.
Malformed JSON is rejected, not silently repaired.

NOT PROVEN · CRITICAL GAPS

Qwen's faithful translation of original NL policy is NOT proven.
Fictional policy completeness / legal correctness is NOT established.
Solver agreement does NOT imply real-world compliance.
Input facts truth is NOT verified.
No claims about real sanctions, customers, transactions, or law.

The solver proves properties of the formal model it is given. It cannot prove that the model faithfully represents reality unless the translation step is itself checked.

M1 — the translation boundary

THE MOST IMPORTANT UNRESOLVED QUESTION

Does Qwen correctly translate natural language to formal logic? Validation mechanisms:

JSON Schema Constraints

Ollama format parameter with structured output. Pydantic validation before solvers. Reject malformed JSON automatically.

Mutation Testing

Generate variants: “over $10K” → “at least $10K” → “exactly $10K”. Verify the formal model changes in expected ways. Detect semantic translation bugs without trusting a second LLM.

Dual-LLM Critic

Llama 3.1 8B as independent reviewer. Compare original NL with Qwen's JSON. Flag discrepancies as warnings — NOT as a hard gate.

Boundary Conditions

Test operators: > vs >= vs ==. Test negations, exceptions, quantifiers.

METRICS

NL → JSON formalization latency (s)     · JSON valid on first attempt (%)     · retries needed
Tokens per formalization                · Mutation sensitivity score: % of mutations producing correct formal changes
Z3/CVC5 agreement rate (%)

Implementation

/root/fol-lab · LOCALHOST:11434

ENVIRONMENT

Path:     /root/fol-lab
LLM:      Qwen3-Coder 30B @ localhost:11434
Critic:   Llama 3.1 8B
Solvers:  Z3 + CVC5
Validation: Pydantic + JSON Schema

OUTPUT STRUCTURE · results/validation_gate/

├── case_A_original/     nl_input.txt · qwen_json.json · schema_validation.json · mutation_diffs.json
│                        z3_result.txt · cvc5_result.txt · metrics.json · final_explanation.txt
├── case_A_mutations/
├── case_B_original/     …
├── case_B_mutations/
├── case_C_original/     …
├── case_C_mutations/
└── summary.md

Decisions

DO / DON'T

Structured outputs. Use Ollama's format parameter with JSON Schema. More reliable than prompt engineering alone.
Mutation testing. Auto-generate semantic variants and verify the formal model changes correctly. Catches translation bugs without trusting a second LLM.
Real solvers. Always use REAL Z3 and CVC5. Never mock the solvers — that defeats the entire purpose.

DON'T

Trust thinking blocks. Qwen3-Coder-30B-A3B does NOT support thinking mode. Don't use <thinking> blocks.
Critic as gatekeeper. The second LLM is advisory only. Disagreement → flag for review. Agreement → NOT proof of correctness.
Save chain-of-thought. Save structured justifications (source_clause → extracted_rule → operator → threshold), not internal model “thoughts”.

Readiness

M1 → M1.5

▚ DONE

[PASS] Basic pipeline working
[PASS] All formal tools installed and verified
[PASS] Three test cases passing

▚ IN PROGRESS / PLANNED

[WIP] Translation boundary validation — M1.5
[PLAN] Mutation testing engine

▚ TODO

[TODO] Human-in-the-loop checkpoint
[TODO] Unit tests on known cases
[TODO] Monitoring dashboard

Implications

WHAT THIS ARCHITECTURE ADDRESSES

This architecture addresses a fundamental problem in AI safety: how to make LLM decisions auditable and deterministic.

AUDITABILITY

PROOF TRAIL

Every decision has a formal proof trail.

REPRODUCIBILITY

SAME IN → SAME OUT

Same formal constraints → same solver result.

DEBUGGABILITY

SEPARATE ERRORS

When things go wrong, distinguish translation error from logic error.

COMPLIANCE

REVIEWABLE

Formal specifications can be reviewed by humans, lawyers, regulators.

The objective is NOT “make AI regulation deterministic.” The objective is to identify exactly which parts can be made explicit, testable, auditable, and reproducible — and where human/legal judgment remains mandatory.

References

PRIMARY SOURCES ONLY

LINKS

Ollama Structured Outputs — ollama.com/blog/structured-outputs
Z3 — github.com/Z3Prover/z3
CVC5 — cvc5.github.io
Qwen3-Coder — ollama.com/library/qwen3-coder:30b
FOL-languages — First-Order Logic Programming
Sept 2026 — my week sprint · FOL-LAB // Local AI + Formal Methods