Skip to content
@Aevion-ai

Aevion.ai

Formally verified cryptographic infrastructure for AI. Home of Aevion Shield—the first Byzantine AI consensus. Enabling AI to go where it couldn't before.

Aevion

Proof-native governance for autonomous AI systems.
Machine-checked invariants. Cryptographic receipts. Byzantine-resilient consensus.

ProofOS Paper HF Spaces AIMO SDVOSB


Aevion builds the governance layer beneath AI products — the formal, receipted, independently auditable infrastructure that sits between an agent's decision and the world it acts on. Not guardrails. Not classifiers. A proof-native control plane.

The Stack

Layer What It Does Built With
Constitutional Halt Gate Blocks any state transition that fails a declared predicate Lean 4 theorems, kernel-checked at runtime
Receipt Chain Every gating decision emits a SHA-256 content-addressed record ProofDB, canonical JSON, append-only ledger
Agent Counsel Colony Multi-agent adversarial review as standing red-team capability Byzantine + SIFT + DiF + Arbiter (7 agents)
Open-Obligation Surface Machine-readable Gödel register of every unproven obligation Named, categorized, receipt-stamped — no confidence percentages

The Thesis

On June 9, 2026, NIST published a mathematical proof (Vassilev, IEEE S&P) that no finite guardrail set can be universally robust against adversarial AI. NIST's official guidance: transition to a continuous-monitor-and-update security model. The same day, Anthropic launched Fable 5 / Mythos 5 — same model, different access envelopes — and publicly stated universal jailbreak prevention is "likely impossible."

Aevion's architecture was already built to this specification: receipt chain (continuous monitoring), counsel colony (proactive red-teaming), halt gate + human escalation (operational resilience). We do not claim to have defeated the impossibility theorem. We claim to have built the architecture the theorem says you need — and published the exact list of what remains unproven.


Founder

Scott Leishman — Founder & Principal Investigator

U.S. Navy Air Traffic Controller (2003–2014), combat-zone deployment to Camp Lemonnier, Djibouti. M.S. Aeronautics, Embry-Riddle Aeronautical University (2018). B.S. Applied Science and Technology, Thomas Edison State University. B.S. Business Administration - Finance, Southern New Hampshire University. B.S. in progress — Information Technology (Cybersecurity), Arizona State University.

Research. "Air Traffic Control Human Factors with Drones" — M.S. Capstone, ERAU (2018), peer-reviewed for final grade. SHEL model + ANOVA quantitative analysis against NASA Ames simulation data. Tested the hypothesis that UAS incorporation significantly impacts controller performance. Covered workload measurement, NextGen technologies (ADS-B, UTM, LATAS, LAANC), and loss-of-separation risk thresholds under BLOS automation — direct intellectual precursor to Aevion's Koopman ρ threshold derivation for autonomous system drift detection.

Additional graduate research (2015–2019): ScanEagle risk assessment (MIL-STD-8820), BLOS operations and SATCOM human factors, GCS automation and skill retention, detect-and-avoid separation technologies. Full archive: unmannedac.blogspot.com.

Operational aviation safety discipline — where traceability, command authority, and zero-failure operating discipline are mission-critical — now formalized as machine-checked proof obligations for autonomous AI systems.


Repositories

Repo Audience Content
ProofOS Public Constitutional halt gate, receipt chain, ModelAccessEnvelope, paper, schemas
Aevion-Verifiable-AI Private Full Lean 4 corpus (1,283 theorems), ProofDB, QKL lattice, EvidenceBench, Agent Counsel Colony

Competitive Validation

Signal Result Date
Kaggle AIMO Progress Prize 3 Top 5.7% worldwide (235 / 4,138) 2026
EvidenceBench-ArXiv 10 papers, 22 claims, all PRIMARY_CONFIRMED 2026
Lean Build Receipt Bridge lake build EXIT=0, source authority chain → PROOF_LEVEL 2026

Company

Aevion LLC — Service-Disabled Veteran-Owned Small Business
CAGE: 15NV7 · UEI: JFCXAGHB3QM6 · St. Cloud, MN
NIST AI Consortium applicant · SBIR/STTR eligible
Contact: scott@aevion.ai · aevion.ai


Theorem where provable. Assumption where modeled. Hypothesis where empirical.
Receipt where observed. Gate where safety-critical.

Popular repositories Loading

  1. .github .github Public

    Organization profile and community health files for Aevion.ai

  2. ProofOS ProofOS Public

    Receipt chain for Lean 4 proof obligations. Constitutional halt gate, ModelAccessEnvelope, Agent Counsel Colony. Backed by seL4/HACMS/CertiKOS verified-systems lineage.

    Python

Repositories

Showing 2 of 2 repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…