Milestone 01 — 2026.09.01-04 // Olares One
←before: FreeToken →next: AI Regulation revolut.hot

FOL-Lab x AI

Formal Methods + Local AI. Making decisions auditable, testable, and deterministic.

Z3 5.1.0 CVC5 1.3.4 Qwen3-Coder 30B M1 Complete

// Mission

Build a hybrid system where local LLMs translate natural language to formal specifications 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

01Natural Language PolicyHuman-readable rules
02Qwen3-Coder 30BNL → Structured JSON
03JSON Schema ValidationPydantic / deterministic check
04Mutation TestingBoundary condition verification
05Z3 + CVC5 SolversIndependent SAT/UNSAT evaluation
06Result ComparisonAgreement check
07Qwen ExplanationFormal result → Plain English

// Toolchain

Z3 5.1.0

Microsoft SMT solver — Python API

CVC5 1.3.4

Independent SMT solver — Python API

SWI-Prolog 9.0.4

Logic programming engine

Soufflé 2.5

Datalog engine for provenance

Clingo 5.8.2

Answer set programming

Lean 4.33.1

Theorem prover with Lake build

All tools verified

// Milestone 1 Results

Case A — ALLOWED

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

SAT
Z3
SAT
CVC5
ALLOW
Decision

Case B — BLOCKED

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

UNSAT
Z3
UNSAT
CVC5
BLOCK
Decision

Case C — POLICY CONTRADICTION

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

UNSAT
Z3
UNSAT
CVC5
BLOCK
Contradiction

// Proven

  • 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

// Limitations

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 — Translation Boundary

The most important unresolved question: Does Qwen correctly translate natural language to formal logic?

Validation Mechanisms

01 // JSON Schema Constraints

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

02 // Mutation Testing

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

03 // Dual-LLM Critic

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

04 // Boundary Conditions

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

Metrics

// Implementation

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: Structured Outputs

Use Ollama's format parameter with JSON Schema. More reliable than prompt engineering alone.

DO: Mutation Testing

Auto-generate semantic variants and verify formal model changes correctly. Catches translation bugs without trusting a second LLM.

DO: 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.

DON'T: Critic as Gatekeeper

The second LLM is advisory only. Disagreement → flag for review. Agreement → NOT proof of correctness.

DON'T: Save Chain-of-Thought

Save structured justifications (source_clause → extracted_rule → operator → threshold), not internal model "thoughts".

// Readiness

  • [PASS] Basic pipeline working
  • [PASS] All formal tools installed and verified
  • [PASS] Three test cases passing
  • [WIP] Translation boundary validation — M1.5
  • [PLAN] Mutation testing engine
  • [TODO] Human-in-the-loop checkpoint
  • [TODO] Unit tests on known cases
  • [TODO] Monitoring dashboard

// Implications

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

Auditability

Every decision has a formal proof trail.

Reproducibility

Same formal constraints → same solver result.

Debuggability

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

Compliance

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