Post-quantum cryptography · machine-checked proofs · privacy & opsec tooling

I build post-quantum security tooling that comes with its own proof of correctness. The recurring pattern across this account: take a real-world security problem — messaging, on-chain signatures, endpoint forensics, running an LLM over untrusted files, surviving a hostile network — implement it against the modern PQC suite (ML-KEM, ML-DSA, SLH-DSA, AES-256-GCM, SHA-3), and then pin the part that matters to a machine-checked proof (Lean 4, EasyCrypt, Coq, Gobra) or a model checker (Z3/SMT, TLA+, Alloy) so the security claim is something you can verify, not just trust.

Everything here is local-first, no-telemetry, opsec-conscious — including the tool that manages the identities these repos are pushed under.

Most of this is experimental, pre-release, and explicitly not audited or certified. Where that's true, each repo says so loudly and states its real threat model up front.

🔎 Browse everything with live descriptions, README snippets and download links → pq-cybarg.github.io

Post-quantum, end-to-end-encrypted, forward-secret chat over Tor (CLI/TUI).

• What it does — Establishes forward-secret sessions secured with the CNSA 2.0 suite (ML-KEM-1024 key exchange, ML-DSA-87 signatures, AES-256-GCM) in pure Rust, and carries them over Tor from a terminal client.
• Why it exists — A usable reference for harvest-now-decrypt-later-resistant messaging when you commit fully to the CNSA 2.0 algorithm set and a CSfC-style layered architecture — with the limits (not FIPS-validated, not accredited, not audited) stated up front instead of oversold.

FIPS-205 SLH-DSA verifier for the Sui blockchain, with a Lean 4 machine-checked spec.

• What it does — An on-chain post-quantum signature verifier (SLH-DSA / SPHINCS+, FIPS-205) written in Sui Move, backed by a Lean 4 formalization and bytecode-equivalence proofs — shipped inside a broad Sui workspace (SDK, wallets, Walrus, Seal, DeepBook, zkLogin, oracles, bridge, and contract-layer PQ authorization primitives).
• Why it exists — Smart-contract platforms have no native post-quantum signatures; this demonstrates a contract-layer PQ verifier whose correctness is machine-checked rather than merely tested, so a chain can gate value behind quantum-resistant signatures today.

ML-ADSA — a trapdoor-free, BLS-like aggregate signature that stays post-quantum.

• What it does — Publishes the documentation for ML-ADSA: a trapdoor-free aggregate signature over ML-DSA-87 (FIPS-204) that compresses many signers into one short signature like BLS, but post-quantum — machine-checked across EasyCrypt, Coq, and Gobra.
• Why it exists — Aggregate signatures today are dominated by BLS, which is not quantum-safe. This is a defensive publication of a PQ alternative, inviting independent cryptanalysis. (Implementation repo is private; this is the public record.)

Cross-platform endpoint forensics suite that runs entirely on your machine.

• What it does — Collects artifacts, stores them in a dual SHA-256 + SHA3-256 hash-chained evidence store, and runs 32 detectors (a defensive mirror of every offensive kill-chain phase) with local-LLM triage — emitting ML-DSA-65-signed evidence and reports. 337 tests; macOS/Linux/Windows.
• Why it exists — Responders need defensible, court-credible local forensics that don't phone home and can't be silently altered. Codified ethics + PQ-signed chain-of-custody make the output trustworthy with zero cloud dependency.

Sandboxed-LLM file/project analyzer with a machine-checked IO boundary.

• What it does — Runs a local LLM (llama.cpp / Ollama / MLX) against a file or directory inside an OS-level sandbox (Landlock+seccomp+ns, Seatbelt, AppContainer, rootless podman), with a Rust typestate that statically prevents untrusted bytes from ever reaching argv / env / paths / URLs / DNS — plus a Lean 4 proof that the boundary holds for every well-typed program. No network egress during analysis.
• Why it exists — "Analyze this untrusted file with an LLM" is a prompt-injection and exfiltration minefield; seck turns the safe boundary into a compile-time and machine-checked guarantee.

Reverse-tethering, privacy-chain, and threat-detection app for Android.

• What it does — Built for hostile networks (e.g. security conferences): reverse-tethers the phone through a laptop; routes traffic through a self-composed privacy chain (WireGuard, Mullvad with PQ tunnels + DAITA, Nym's Sphinx mixnet, Tor with the full obfs4/meek/webtunnel/conjure bridge stack); detects IMSI catchers, evil-twin APs, BLE trackers and permission drift; and offers a one-toggle conference lockdown with attestation snapshot, honeypot, tamper-watcher and an incident-response runbook.
• Why it exists — At a conference the local cellular/Wi-Fi can't be trusted. This puts reverse-tethering, post-quantum VPN chaining, and on-device threat detection behind a single hardening switch.

The multi-identity GitHub safety tool — this profile was published with it.

• What it does — ghid is a CLI that forces identity-aliased SSH URLs (git@github-<id>:owner/repo), locks a repo to one identity via a pre-push hook, verifies the identity GitHub actually sees, and rewrites remotes; ghidbar is a macOS menu-bar companion showing the current repo's bound identity.
• Why it exists — GitHub authenticates SSH by key fingerprint, not the cosmetic User field — so a machine with several identities will silently push under the wrong account. ghid makes that mistake impossible.

A formally-verified anatomy of the AI capital loop.

• What it does — A forensic analysis of the circular funding among the major AI/compute firms, with the falsifiable core proven by four independent engines (Tarjan SCC, Z3/SMT, TLA+, Alloy), layered claims that keep proof separate from evidence separate from speculation, an interactive dashboard + globe, and a transparent server-less poll.
• Why it exists — "AI bubble" claims are usually vibes. This pins the structural core to machine-checked proofs and open data anyone can reproduce with bash run_all.sh.

• What it does — A configurable dead-man's-switch system of smart contracts for QRL's Zond (post-quantum) chain: actions that fire automatically if the owner stops checking in.
• Why it exists — Key-recovery and "if I disappear" guarantees need a quantum-resistant settlement layer; QRL Zond provides one. (Early-stage.)

• Reserved, early-stage repo (license only today) — placeholder for forthcoming QRL/Zond work.