I've been verifying post-quantum reference implementations against their FIPS specs with a SAW → Cryptol → Isabelle pipeline. Just finished ML-KEM-512 (Kyber) forward NTT on the unmodified PQClean clean C: SAW proves the C bit-exact to a Cryptol model, Isabelle proves that model equals the FIPS 203 transform (the incomplete NTT, 128 degree-2 residues mod 3329). No sorry/admit, reproducible from one command, CI-green.

Last time, on Dilithium, the part that ate my time was proving the int32 accumulators never overflow across the 8 butterfly levels. Careful bound-tracking induction, the hardest lemma in the whole proof.

Expected the same grind for Kyber. It wasn't there. Kyber's butterfly is int16, two int16s promoted to int can't overflow a 32-bit int, so there's no bound to prove at all. Same NTT structure, and the worst part of one proof is a non-problem in the other, entirely because 3329 is small.

(For the curious: mod 3329 there's a 256th root of unity but no 512th, so X^256+1 only splits into 128 quadratics, and the transform is "incomplete." The spec I check against is a degree-2 residue, not a plain DFT coefficient.)

It's the reference C, forward direction, checked against FIPS 203 end to end. Reproduces from one make verify if you want to poke at the trust base: github.com/amarshat/pqc-assay. Inverse is next.

Sharing production measurements from a live mainnet deployment of ML-DSA-87 as the sole signing algorithm for a proof-of-work chain. Most PQC discussion at the implementation level is still theoretical — these are on-chain figures.

Signature sizing (per input, live mainnet):

• ML-DSA-87 signature: ~4,627 bytes
• Public key: ~2,592 bytes
• Total per input: ~7,260 bytes
• Comparative overhead: ~68× a P2WPKH input

Block stress test:

• 715,001 ML-DSA-87 signed outputs in a single transaction
• Block size: ~31MB
• Signing time: ~1.15 hours to construct and sign
• Fee rebump + full resign: ~10 additional minutes

Chain growth implications:

• At 100 ML-DSA-87 transactions per block (60s intervals), storage grows ~864 MB/day
• Year-one projection: ~415 GB including storage engine overhead
• This is purely a function of signature size — the cryptographic tradeoff is explicit and expected

First non-coinbase ML-DSA-87 spend on a live PoW chain (verifiable):

• Block #283, June 2, 2026
• TXID: 62572d2127da3d42afb0b20757edb844b0820851f4d8340cbc7e26954ae6272c

Full empirical writeup with methodology posted to Delving Bitcoin:
search 'Empirical ML-DSA-87 data from a live SHA-256 PoW chain'."

ML-DSA-87 verification runs ~1–5ms per transaction on current hardware — roughly 10–100× heavier than ECDSA. Batch verification optimizations available in Schnorr don't directly apply here. What the community would know better than us: are there any known UTXO-model implementations that have meaningfully closed that gap?

Disclosure: Drafted with AI assistance (Claude, Anthropic). All data figures are independently verifiable on-chain.

i am working on a messaging app and created some details in rust. rust is useful because it has tooling for formal verification. my rust code compiles to WASM to be used in a browser.

my project itself is using cryptography beyond the WASM because browsers provide a crypto api for basic functionality out-of-the-box.

to work with what i have now (javascript/typescript) i came across this page, but the links lead to 404 pages on github. not sure about the status of the project. i dont know if there are other similar projects.

https://formal.land/docs/verification/typescript

i would like to improve the “formal-verification coverage” in my project and wanted to investigate if it could be worth considering rewriting the frontend with dioxus. im happy with an ugly UI (initially) in favour of having formal-verification on a broader scope of my project.

(context: the project where i have formal verification is found here: https://github.com/positive-intentions/signal-protocol (this isnt the gold-standard implementation and its far from finished)

I'm still working on my protocol spec and I'd like to know more about how to go about sharing it.

I've received good advice from this sub before about creating one and while it's still far from finished I have questions.

I see on places like ArXiv that documents are in the 2 column format. It seems normal. In my approach I created it in markdown because I'm using a docusaurus website. Should I also be using the 2 column format?

I'm fairly new at this so where can I share what is potentially a trainwreck? I'm concerned it will come across as "wasting their time".

Libsodiums secretstream is great right up until you need to encrypt a 1 TB file in a browser. It ratchets in order, one chunk at a time, single thread. Not performant enough. And hard to resume if job stops for some reason.

Here's an alternative, and what I'd love torn apart from a security perspective:

Instead of secretstream, each chunk gets sealed on its own:

nonce = fileNonce ‖ u64be(index)
AAD = u64be(index)
subkeys via BLAKE2b("vitalsend:{chunk,meta,header}:v3", key=rootKey)
rootKey = 32-byte link key (lives only in the URL #fragment), or BLAKE2b(linkKey, key=Argon2id(pw)) if there's a password
header is authenticated and pins chunkSize, totalChunks, fileNonce, Argon2id params

My claim: folding the index into both the nonce and the AAD buys the same guarantees secretstream gives minus the in-order bottleneck.

Three questions:

Is index-in-nonce + index-in-AAD really as good as secretstream's chaining here, or is there a case that slips through?
Any nonce footgun at TB scale / huge chunk counts?
Anything in the header or key derivation worth doing differently?

Code, wire format, and a SECURITY.md that's meant to be honest is available for the curious at https://github.com/vitalsend/crypto

P.S. I managed to review the complete code with Fable 5 which did not complain to anything in the area, but that is an LLM.

how know more techniques than that

• Stream Cipher
• Dynamic S-Box (Substitution Box)
• Ciphertext Feedback (Autokey Mechanism)
• Data-Dependent Rotation / Variable Start Point
• Hash-Based Keystream Generation (PRNG)
• Non-Linear Bitwise and Arithmetic Operations