PerceptraAI
Contact Lab
PERCEPTRAAI RESEARCH LAB · FORMAL SYSTEMS GROUPPEER VERIFIED

Foundational research in bounded autonomous systems.

PerceptraAI's research group investigates the mathematical boundary between probabilistic models (LLMs, neural vision) and deterministic physical or financial systems. We publish specifications, proofs, and production-tested benchmarks.

FEATURED FORMAL RECORDZENODO 23214596

DARM Core Research & Machine-Checked Calculus

DARM Core v1.0 is PerceptraAI Lab's machine-checked research foundation for boundary-indexed assurance transfer. Visit the dedicated research page within the DARM mini-website for theorem proofs (E35, E36, E37), runtime trust boundaries, repository evidence, and the Zenodo archived record.

Open DARM Research Page →DARM Evidence & Guard Overview
DARM RESEARCH RECORD METRICS
  • Paper TitleDARM Core v1.0
  • AuthorOlusanya Gbolahan V.
  • Proof EngineLean 4 Machine-Checked
  • VenueZenodo #23214596 ↗
RESEARCH FOUNDATION

Laboratory Axioms

REF: LAB-01 TO LAB-03
Axiom 1: Probabilistic models must never hold mutable state or physical credentials directly.

All action intents are treated as untrusted proposals. Authority must be validated deterministically by a distinct verification kernel with static mathematical guarantees.

Axiom 2: Edge intelligence must survive total network partitioning without degradation.

Systems deployed into physical infrastructure (CCTV, banking switches, physical access) must maintain continuous detection, decision logging, and alarms with zero internet access.

PUBLICATIONS & SPECIFICATIONS

Technical Papers & Drafts

OPEN ACCESS SPECIFICATIONS
  • DARM-CORE-V1OCTOBER 2026
    PROVED

    DARM Core: A Machine-Checked Calculus for Boundary-Indexed Assurance Transfer

    Olusanya Gbolahan V.

    PerceptraAI Lab formal research paper (v1.0, Zenodo Record 23214596, 12 pages). Establishes a machine-checked Lean 4 calculus for transporting assurance claims across agent-system boundaries with representation adequacy, compositional obligations, and heterogeneous warrants.

    Read Full Specification →
  • WP-2025-04DECEMBER 2025
    TESTED

    Sub-150ms P99 Scoring Paths with In-Process ML & Statutory AML Reporting

    Vigil Engineering Team

    An empirical analysis of pay-as-you-go serverless fraud detection architectures on GCP. Compares in-process inference against remote prediction endpoints.

    Read Full Specification →
  • WP-2025-03OCTOBER 2025
    PROVED

    WASM Perception Sandboxing: Bounded Memory and Trapped Syscalls

    PerceptraAI Edge Systems Lab

    Formal verification of WebAssembly sandbox isolation for computer vision neural network inferencing on resource-constrained physical edge hardware.

    Read Full Specification →