Most cryptography libraries ask you to trust their code. Ours is machine-checked: 59 F* modules verify with zero assume and zero admit — and we publish what is still missing: 47 trivial lemmas, a stub AES-GCM model, and no machine-checked link to the shipped Rust.
Part of the AIvantGuard SDK — tier-based licensing, usable standalone.
Adversaries record your encrypted traffic today, waiting for quantum computers to decrypt it tomorrow. Data with a long secrecy lifespan is already compromised — unless it is post-quantum encrypted now.
"We implemented Kyber" is not assurance. In agentic AI it gets more serious still: agents mostly work with clear-text files. Machine-checked formal proofs are the difference between hope and evidence.
Round-3 Kyber-1024 — post-quantum key encapsulation. ML-KEM-1024 lands in ABI 1.3.
Round-3 Dilithium-5 — post-quantum digital signatures. ML-DSA-87 lands in ABI 1.3.
Authenticated encryption with additional authenticated data (AAD); J0 derived per SP 800-38D for non-96-bit nonces. Shipped in ABI 1.2.0.
59 F* modules verify with zero assume val and zero admit — after we found and removed a vacuous verification in our own earlier tree. 47 trivial lemmas remain, the AES-GCM model is a stub; the EAL7 artefact set is produced in-house, no laboratory has assessed it.
Runs safely inside web applications — post-quantum encryption client-side, in the browser, with no server-side trust required.
Shipped binaries are compiled through a VM-based virtualisation layer. CI proves the virtualised build is digest-identical to the native build, so obfuscation cannot silently change behaviour. The source is not distributed; the layer raises the cost of reverse engineering — it is not a proof of unbreakability.
Hardened runtime memory handling shields secret material while it is in use — defense in depth on top of the formal proofs. Zero external runtime dependencies.
Our own construction: multi-party computation across cooperating nodes — decryption and modification require consensus. Proprietary AIvantGuard IP; research status, not part of the shipped ABI.
aioneguardcrypto is the post-quantum backbone of the entire stack — GuAIrdIAn's mobile transport, the agentic infrastructure's encrypted configurations, and the Wallet's future foundations all run on it. One verified foundation under everything.
8 platform families — macOS, Linux (glibc and musl), Windows, FreeBSD, OpenBSD, WebAssembly, Android, iOS. Each ships as a signed archive.
macOS
x64 · arm64 · universal
Linux
glibc & musl · x64 · arm64
Windows
MSVC · x64 · arm64
WebAssembly
browser · Node/edge
Android
arm64 · armv7 · x86_64
iOS
device + simulator
FreeBSD
x86_64 · aarch64
OpenBSD
x86_64
C, C++, Rust, Python, Node/TS, Go, .NET, Java, Kotlin, Swift — golden-tested against every release. ABI v1.1 adds an ASN.1/DER encoder-decoder for certificate-path integration.
Install & quickstart, generated API reference, guides: key management, encryption, signing, security notes, support matrix, migration.
Machine-readable API spec (single source of truth) with a generated llms.txt + full agent corpus — your coding assistant integrates it too.
C quickstart, C++ round-trip, Web demo, Android & iOS sample apps — encrypt→decrypt verified end to end.
Delivered as signed archives — SHA-256 checksums, GPG signature and a CycloneDX SBOM on every release (current: v1.0.0). Licensed to customers; pricing follows the dialogue.
F* modules verify — zero assume, zero admit. 47 trivial lemmas remain
EAL7 artefact set produced in-house, inspectable and re-checkable. On request we support a customer's certification: audit support and the code changes an evaluation requires. No laboratory engaged today.
Kyber-1024 + Dilithium-5. NIST vectors pass for SHA-3, DRBG, AES-GCM, HMAC/HKDF; the PQ primitives are checked against reference KATs, not NIST vectors. No FIPS certification.
Fuzzing executions, all runs, lower bound · 20 targets since March 2026 · 555 crash artifacts found and fixed · own campaign
Complete
Round-3 Kyber-1024 + Dilithium-5, stable C ABI 1.2, GPG-signed releases, VM-virtualised builds with digest-verified equivalence.
In progress
Formal proof that the virtualisation layer preserves semantics — the layer that protects the shipped binaries.
Status: proof in progress
Then
The final NIST standards, added as new ABI symbols in ABI 1.3 — additive, the round-3 symbols stay.
Long term
Any track a procurement requires — Common Criteria, FIPS 140-3 / CMVP or ACVP — is started on that demand. The evidence set is kept current, so an evaluation starts from a complete package, not from scratch.
Quarterly security update releases · recurring vulnerability assessments across the full primitive set · coordinated disclosure policy · every release checksum-verified and cryptographically signed.
Banks and enterprises replacing RSA/ECC before Q-Day — with DORA-relevant compliance.
Where a crypto bug is a safety event: formal proofs are the requirement, not a luxury.
Machine-checkable assurance for auditors and regulators — evidence, not marketing.