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

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

Example: HIPAA Compliance Pipeline

HIPAA compliance involves two distinct challenges: detecting Protected Health Information (PHI) and verifying that disclosure rules are followed. Aare Edge handles both on-device.

Step 1: PHI Detection (DSLM)

The HIPAA Safe Harbor rule defines 18 categories of Protected Health Information that must be identified and protected. The HIPAA DSLM extracts these identifiers from unstructured text - handling variations in formatting, OCR errors, and natural language phrasing that regex cannot.

Step 2: Constraint Verification (Z3 Lite)

Detection alone isn't enough. HIPAA's Privacy Rule contains 76+ constraints governing when and how PHI can be used or disclosed. Z3 Lite evaluates these constraints against the extracted entities:

• Minimum Necessary: Only the PHI required for the specific purpose may be disclosed
• Authorization Requirements: Patient authorization required unless a specific exception applies
• Treatment/Payment/Operations: Permitted uses without authorization for TPO activities
• Business Associate Rules: Third-party access requires BAA and use limitations
• De-identification Standards: Safe Harbor (remove 18 identifiers) or Expert Determination
• Patient Rights: Access, amendment, accounting of disclosures
• Breach Notification: Required actions when unauthorized disclosure occurs

The Complete Pipeline

This entire pipeline runs on-device in under 100ms. No PHI leaves the device. Mathematical proof of compliance or violation.

Performance Profile

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

Deployment Targets

Cloud vs. Edge: When to Use What

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

SDK Components