A Verified Axiom is a deterministic Python class that dictates how D.I.A.N.A. OS extracts parameters from unstructured LLM generation and proves their safety via the Microsoft Z3 SMT Solver.
Rather than relying on vague natural language prompt engineering, Verified Axioms act as an impenetrable mathematical fence. They force the local Ollama LLM to output strictly typed JSON, bound its logical conclusions via Pydantic validators, and evaluate safety limits natively before executing any physical or digital action.
In critical infrastructure, engineers write Axioms to sit directly between the LLM and the execution hardware. The system follows a strict Pydantic Chain-of-Thought pipeline:
D.I.A.N.A. forces the underlying LLM to generate parameters that perfectly match a strictly typed Pydantic Schema. If the LLM hallucinates an invalid key or a string instead of a float, the payload is immediately rejected.
Once the parameters are extracted, they are passed into the Z3 SMT (Satisfiability Modulo Theories) solver. The solver mathematically proves whether the generated parameters violate hardcoded algebraic safety constraints (e.g. maximum voltages, kinematic limits, financial exposure boundaries).
Select an architectural pillar and a sector to view the drop-in Pydantic + Z3 scripts.
import z3
from pydantic import BaseModel, Field, field_validator
from diana_os.historian import SQLiteLedger
class ClinicalTrialIngest(BaseModel):
patient_id: str = Field(..., description="Anonymized patient hash")
dosage_mg: float = Field(..., description="Calculated chemotherapy dosage")
@field_validator("dosage_mg")
def verify_dosage_safety(cls, v):
solver = z3.Solver()
dosage = z3.Real('dosage')
# Absolute physical limit for human biology
solver.add(dosage == v)
solver.add(dosage <= 150.0)
solver.add(dosage >= 10.0)
if solver.check() == z3.unsat:
SQLiteLedger.commit_violation("DOSAGE_LIMIT_EXCEEDED", v)
raise ValueError(f"HARD UNSAT: Dosage {v}mg exceeds physical biological limits.")
return vRun the axiom in dry-run mode to verify the Z3 solver constraints natively:
python3 -m diana_os.verify --module axioms.clinical_ingest[SUCCESS] Axiom syntax valid. Z3 UNSAT conditions successfully compiled.
To launch the orchestrator on a local air-gapped node:
python3 -m diana_os.orchestrator --execute axioms.clinical_ingest