aare.ai - Aare Verify Edge

Formal Verification Without Connectivity

Aare Verify Edge brings the same mathematical guarantees of our cloud API to environments where network connectivity isn't available or data cannot leave the device. Purpose-built for constrained environments with limited memory, compute, and power.

Instead of sending LLM output to a server, Edge runs a complete verification pipeline on-device: a Domain-Specific Language Model (DSLM) for entity extraction, and Z3 Lite for constraint solving. Same inputs, same outputs, different implementation.

Architecture

Input

LLM Output

→

Extract
DSLM

→

Verify
Z3 Lite

→

Output

Proof

Domain-Specific Language Models

A DSLM is a small model fine-tuned for one task: extracting the entities and patterns that matter for your specific validation domain. Unlike general-purpose LLMs, DSLMs are focused, quantized, and optimized for on-device inference.

Single model vs. complex pipeline: One inference call replaces regex, keywords, enums, and confidence scoring
Domain-specific: A DSLM for healthcare doesn't know poetry. It knows PHI categories, treatment codes, and authorization requirements
Quantized and compiled: 4-bit quantization, CoreML/ONNX compilation for efficient device hardware utilization
Handles variability: Voice transcriptions, OCR output, user-typed text - the DSLM handles linguistic variability that patterns can't

Z3 Lite: Right-Sized Verification

Full Z3 is a powerful SMT solver that can handle arbitrary satisfiability problems: quantifiers, arrays, bit vectors, floating point. For policy verification, you don't need that machinery.

Z3 Lite is a purpose-built constraint solver for bounded policy verification:

Boolean logic, comparisons, basic arithmetic - the operators that actually appear in compliance rules
No solver configuration or timeouts - evaluates known constraint structures in milliseconds
Native implementation: Swift on iOS, Kotlin on Android. No Python runtime, no external dependencies
Same guarantees: SAT/UNSAT with proof trace. The mathematics is identical; the implementation is lighter

Performance Profile

Component	Metric	Value
DSLM	Base model	Phi-3-mini with LoRA fine-tuning
	Quantization	4-bit
	Model size	~500MB
	Inference time	20-50ms
Z3 Lite	Binary size	<1MB
Z3 Lite	Evaluation time	<10ms
Total SDK	Cold start	~500ms
	Warm validation	<100ms
	Runtime memory	~200MB

Performance varies by domain. A DSLM for simple entity extraction will be smaller than one handling complex semantic boundaries.

Deployment Targets

📱

Mobile Apps

iOS and Android native SDKs. Validate LLM responses in-app without network round-trips.

🏭

Industrial IoT

Edge gateways, industrial controllers, and embedded systems. Validate before transmitting to cloud.

🔒

Secure Enclaves

TEEs, air-gapped servers, HSMs. Environments where external dependencies aren't allowed.

🚗

Automotive

In-vehicle systems with limited connectivity. Real-time validation for voice assistants and displays.

🏥

Medical Devices

FDA-regulated environments requiring on-device validation without cloud connectivity.

⌚

Wearables

As LLMs move to watches and glasses, validation follows. Efficient enough to run on a watch.

Cloud vs. Edge: When to Use What

Use Aare Core (Cloud/On-Prem)

• Can make API calls

• Input is structured LLM output

• Zero ML overhead preferred

• Rules are well-defined patterns

• Connectivity is reliable

Use Aare Edge

• Data cannot leave device

• Input may be noisy/variable

• Connectivity is unreliable

• Validation embedded in device

• Air-gapped environment

They're not competing approaches. They're the same formal verification thesis,
implemented for different deployment constraints.

SDK Components

Z3 Lite Solver

Native constraint solver for iOS (Swift) and Android (Kotlin). MIT licensed.

DSLM Runtime

CoreML integration for iOS, ONNX for Android. Efficient on-device inference.

Healthcare POC

HIPAA Safe Harbor DSLM (18 PHI categories). Reference implementation with ontology and training pipeline.

Custom Domain Training

DSLM training toolkit for your specific domain. Build validators for any compliance requirement.