Architecture

Vera's architecture follows from a single design rule: the LLM never decides. Language models translate; a deterministic solver decides; an agent acts. Every layer exists to enforce or exploit that separation.

The layers

Layer	Technology	Responsibility
Ingestion	REST connectors	Pull jobs, schedules, vehicles and personnel from the customer's systems (FSM, TMS/ERP, telematics) into a normalized internal view.
Language	Model-agnostic LLM + schema validation	Translate free text — rules, disruption reports, chat — into typed, validated structures. Output is checked against Pydantic schemas; invalid output is repaired or rejected, never passed through.
Memory	Knowledge graph (Neo4j) + PostgreSQL + vector index	Entities, relationships, rules and full decision history. Semantic recall selects the rules and precedents relevant to each decision.
Reasoning	Z3 constraint solver	Check every candidate plan against every applicable rule. Deterministic: same facts and rules, same verdict. Produces unsat cores for infeasible plans.
Agent	MCP-based runtime	Plan multi-step resolutions, call tools, execute at the configured autonomy level (suggest / approve / autonomous).
Interfaces	Console, REST, MCP	The operator product and the component surface share one engine contract.

Why translation and decision must be separate

A language model is a probabilistic system. Used as a decision-maker, it can violate a constraint with nonzero probability on any given day, and its explanation of why it decided something is a plausible narrative, not a causal account.

Used as a translator into a typed schema, the same model becomes auditable: its output either validates against the schema or it doesn't, a human confirms the structured form of every rule before activation, and the extraction step can be benchmarked precisely (see the validation evidence in the GitHub documentation).

Once facts and rules are structured, the decision is computed by Z3 — a solver whose answers are reproducible and whose rejections come with a minimal proof of impossibility (the unsat core). This is what makes Vera's explanations compliance-grade: they are read off the proof.

Memory as an operational asset

Every rule, fact and decision accumulates in the knowledge graph. This has two consequences:

1. Recall — when a new disruption arrives, Vera retrieves the rules and similar past decisions that apply, so the solver checks the right constraints.
2. Institutional knowledge — the rulebook plus decision history is effectively the company's operational expertise in machine-checkable form. It survives turnover and is queryable (vera_query_memory over MCP, or the Memory surface in the console).

Deployment shape

The whole system runs as Docker services on modest hardware: 4–8 vCPU, 16–32 GB RAM, 50–100 GB storage. No GPU is required — model inference is either a hosted endpoint or a customer-managed open-weight model (Mistral family, Teuken class, via Ollama). See Deployment.