I asked AI to write a cryptography library — here's what kept it mostly honest

A couple of weeks ago I wrote about my take on AI: treat it like any other tool, judge it by results, and keep enough of your own understanding to notice when it’s wrong. What I didn’t mention: that take didn’t come out of nowhere — the project below was already underway when I wrote it, and it’s the most direct answer I can give to “so what are the results?”

It’s called ai_crypto_lib — aicl for short, a name the agent came up with on its own — and it’s a security-hardened C23 shared library implementing 24 public cryptographic modules — the AES family, SHA-2/SHA-3/SHAKE, BLAKE2b/BLAKE3, ChaCha20-Poly1305, SipHash, Argon2, Ed25519/X25519, ML-KEM, and the RFC 10042 PQ/T hybrid combiner.

Every line of it was written by AI coding agents. Not “mostly” — a rule of the experiment was that I could not write, delete, or edit any code directly, not once. I didn’t write the NTT, the field arithmetic, or the S-box circuits; I couldn’t have. My role was operator: rulings, specification input, and spot checks.

Before anything else, the part that matters most:

Do not use this library for anything real. It has received no independent human cryptographic or security review, and AI-generated cryptographic code must be assumed unsafe until proven otherwise by qualified humans. It is a research project — the honesty of its claims is itself under test.

With that on the table, here’s what the experiment actually is.

The question

Can an AI coding agent produce high-quality, security-critical C code if you stop prompting and start engineering constraints around it? Not “vibes plus a test suite,” but the full apparatus a necessarily paranoid C project deserves: coding standards, formal verification, quality gates, cross-model review — with the human reduced to an operator who rules on disputes and feeds in specifications.

The rig is concrete: the pi coding agent harness, configured with subagents — GLM-5.3 as the main orchestrator, and mostly GLM-5.3-Flash as the workers (the same budget-friendly speedster that earned its name-check in my last post). One model plans and delegates; a cheaper, faster sibling executes. And around both sits the constraint that defines the experiment: the human cannot touch the code. Every write, delete, and edit in the repository flows through an agent.

Crypto is the most exacting test domain. The code either matches FIPS 197 (AES) to the byte or it doesn’t. It’s either constant-time or it leaks. A subtly wrong memset is a CVE. There’s no sliding by on plausible-looking output — which is exactly the failure mode people (rightly) suspect LLMs of.

The ground rules

Three rules shaped everything:

A strict priority order: correctness first, then side-channel resistance, then speed. Never sacrifice a higher one for a lower. This is why the AES implementation is deliberately slow — more on that below.
Original implementation only. No copy-paste from anywhere — not Stack Overflow, not vendor blogs, not other LLM output. And for the initial implementation of each algorithm the rule was stronger than “don’t copy”: don’t even look. The agent was told to generate every algorithm directly from its specification, without consulting anyone else’s implementation — and the same applied to constant-timedness: the secret-independent constructions could draw on known technique, but had to be built by the agent rather than cribbed from existing constant-time libraries. The starting point enforced this mechanically: I began from specification documents out of which any C code had been stripped — pseudocode stayed — except where the C was the sole source of the information (deleting that would delete knowledge, not a crutch). The agent reads e.g. FIPS 203 (ML-KEM) and writes its own C23. Spec-mandated constants and official test vectors are data, not code, and are fine to consume. Third-party snippets carry license contamination risk, can embed subtle bugs or deliberate backdoors, and can’t be honestly verified by a prover run over code nobody fully understands.
The standards are machine-enforced, not aspirational. At the core sits AGENTS.C.md — a coding standard I’d been curating for about a year before the experiment started; in effect, my coding standard, finally put to work. It folds in CERT C and its ISO distillation, ISO/IEC TS 17961, the CWE Top 25, and MISRA C:2012 guidance, and is pinned as a digest whose SHA-256 is checked by a gate — drift or absence fails the build. Fixed-width integers only, memset_explicit for secret wipes (backed by a relaxed-atomic store pass the optimizer can’t remove), opaque handle types, mlock-pinned secrets with fail-closed refusal if the lock is denied.

Fifteen gates between commit and “green”

The heart of the project is a fail-fast gate chain. One command, fifteen gates, in order:

Unit and integration tests under ASan/UBSan, then again at -O3, then again under Clang with -Werror.
Clang static analyzer with zero findings required.
annocheck ELF hardening notes (PIE, relro, CET, fortify).
Doxygen with warnings-as-errors.
Coverage enforced at ≥85% lines and branches (currently 95.9%/87.3%).
CBMC bounded model checking — 133 discharged proof harnesses.
Frama-C WP deductive proofs over ACSL contracts — 24 harnesses.
Coding-standards, constant-time, fuzzing, Lean, ThreadSanitizer, and Rocq gates, each with its own zero-tolerance bar.

The known-answer testing is where correctness gets its teeth: the library is verified record-by-record against official NIST corpora — 47,250 GCM vectors, 2,078 AESVS KAT records, 1000-iteration Monte-Carlo chains, the ACVP ML-KEM and FIPS 202 (SHA-3/SHAKE) suites — all fetched by a script that SHA-256-pins every artifact so a fresh clone verifies known answers without trusting the network.

And my favorite detail in the whole pipeline: a run that verifies zero official vectors while corpora are missing fails the gate. A PASS that verified nothing must not be green. Skips are loud, counted, and fail-closed.

Formal verification, with honest accounting

“The library is formally verified” would be a lie, so the README doesn’t say it. Instead there’s a verified-surface table, and every claim in it is auditable:

The 133 CBMC harnesses are published as a three-way split: 130 unassisted, 3 assume-gated (their full-width number-theoretic properties are injected as __CPROVER_assume citations, kernel-checked by a Lean proof tree, and bridged by reduced-width no-assume checks), and 20 parked — harnesses where the solver hits measured walls, each parked with its wall measurements, resume levers, and compensating evidence documented in-tree.
The CBMC tier verifies a generated C11-compatibility mirror of the C23 sources, not the shipped binary — and the mirror has caught real divergences in the project’s history, so it’s treated as a live risk, machine-audited on every run.
A green constant-time verdict comes with a written admission of what it does not show: the dudect-style Welch t-test harness measures intra-process timing distributions, cannot observe attacker-driven cache eviction channels by construction, and a sub-band reading is attributed to host noise by a reviewed noise model — engineering judgment, not proof.

That last bullet deserves emphasis because it’s the thesis of the whole project. The constant-time gate runs 39 instrumented targets through 2²⁰ samples per class, requires an injected deliberately-leaky positive control to be detected or fails closed, and still ships with a paragraph explaining the nanosecond-scale residue it cannot rule out. The tooling doesn’t just check the code — it documents the limits of the check.

The honesty engineering

What surprised me most wasn’t the verification depth; it was how much of the project’s texture ended up being claim hygiene. Some examples, verbatim spirit from the ledger:

Gate-run evidence is provenance-stamped (git tree, tool versions, UTC timestamp) and banked, and a stale summary file carries an explicit # STALE-MARKER that a checker script enforces — a stale artifact can no longer read as current truth.
A historical claim about CBMC memory-limit declarations was RETIRED in writing when the mechanism was removed, rather than quietly deleted.
The all-gates-green state of one date is labeled COMPOSED from follow-up runs, not one sweep — because the single-invocation attempt failed mid-chain and the honest provenance is two runs.
Cross-model LLM review (each wave implemented by one model family, reviewed by another, enforced by a diversity-checking script) is explicitly labeled not independent review — models share training data and failure modes, so it’s a diversity control, not cryptographic assurance.

When the subject matter is “can an AI be trusted,” the metadata about how claims decay is itself the product. Every performance figure points at a dated, provenance-stamped benchmark run; every coverage number is recomputed from a machine-readable report rather than quoted from memory.

The operator’s chair

So what did I actually do? The no-direct-edit rule has a consequence that took me a while to appreciate: every human intervention must be expressible as text — a ruling, a spec pointer, a review note — that a model can act on. You can’t “just quickly fix it.” Mostly:

Rulings. The repo keeps an operator-rulings log. Some are architectural (“NIST-curve ECDH permanently excluded; X25519 is the sole curve”), some are deliciously specific (“using a volatile-qualified view as a wipe-elision barrier is a misuse — use relaxed atomic stores”), some are deletions (an entire private HMAC/HKDF module was removed rather than kept half-specified).
Specification input. Which RFC/FIPS documents are normative, and what the reference corpus is.
Spot checks. Enough reading of the agent’s output to keep my own understanding alive — which, per my earlier post, is the whole point of holding the tool.
Tracking. A best effort was made to track every task, decision, and idea in beads (bd). It’s a tool I’ve found indispensable since long before this project and expect to keep finding indispensable here on out — and it’s why the docs can cite rulings, parking decisions, and retired claims by ID: the trail existed before the prose did.

The interesting discovery is that this is a real and distinct job. Constraining an AI agent to produce verifiable security-critical code is systems engineering: you build the gates, the pins, the ledgers, and the fail-closed defaults, and the agent fills in the proof-carrying details. The agent never got bored of writing the fifteenth harness’s documentation stanza. I would have.

In hindsight, the highest-leverage work I did was the year of curating that coding standard before a single line of library code existed. Constraints written in advance scale across every agent that reads them; corrections written after the fact are paid per instance.

Results, and the honest asterisks

Performance is third-priority by decree and the numbers say so: ChaCha20 at ~830 MiB/s and ChaCha20-Poly1305 sealing at ~545 MiB/s (64 KiB), BLAKE3 at ~660 MiB/s — while the AES family runs at ~35–92 MiB/s, roughly 60× slower than AES-NI OpenSSL. That’s not an accident: under the table-free S-box doctrine, SubBytes is computed as branch-free GF(2⁸) circuits (equivalence Z3-proven against the reference tables) so no secret ever indexes memory — an approach the agent had to arrive at on its own: existing constant-time implementations fell under the same don’t-even-look rule as the algorithms themselves, even though the general techniques for building and measuring constant-time code were known territory. Bulk AES throughput belongs to hardware paths; this library is the assurance-graded choice.

That last sentence is where my hindsight lives. The no-intrinsics rule in my coding standard makes hardware AES unreachable — it has no portable C spelling — and looking back, the ban wasn’t a constant-time call (AES-NI and its ARM equivalents are data-independent; a hardware lane wouldn’t violate the second priority) but an auditability one: with the ban in place, every line of the cipher is portable C that CBMC and Frama-C can chew on. If I ran the experiment again, I’d do it differently: keep the portable, table-free lane as the assurance-graded default and make hardware AES a conditional add-in selected by the build target — AES-NI on x86-64, the ARMv8 Cryptography Extension (AESE/AESMC) on aarch64 — sitting behind the same opaque API. One build flavor, hardware lanes where they exist, and the 60× stops being a flat tax on the most performance-sensitive primitive in the library.

The asterisks that matter: the full gate chain has failed on record and those failures are banked and cited, not buried. The 100%-branch-coverage aspiration is documented as not yet enforced. No CI service has ever run — enforcement is a nightly run on my own machine plus committed evidence, and the README says so in bold.

The takeaway

Four years ago I wrote AI off over a broken Hello World. This project is the other end of the arc: an AI agent producing code that survives CBMC, Frama-C, Lean, Rocq, sanitizers, 50,000+ official test vectors, and a statistical timing harness — because it was never asked to be trustworthy. It was made auditable, and trust was left to the auditing, as it should be.

That’s my updated take on AI-assisted engineering: the ceiling isn’t the model’s talent for plausible code, it’s the rigor of the cage you build around it. For security-critical work, spend your human effort on the cage — the standards, the gates, the provenance, the fail-closed defaults. The agent will happily do the rest, fifteen gates’ worth, and never once ask why.

The library stays a research project until qualified humans have reviewed it — which is exactly the kind of claim this project has taught me to state precisely.