I'm not a cryptographer or a cybersecurity expert. I'm a JavaScript dev. I'm interested in cryptography enough for it to become a side project.

Things like unit tests have always been a good idea for professional-grade work and ai has made it easier than ever.

For that extra bit, I want to use AI to create formal verification. Before I get too far, I'd like to ask about your experience with AI in formal-verification. The following is what I got so far.

https://glitr.io/docs/technical/formal-verification

As I learn how it works, I have a few questions about the approach.

- is it invalid because it's vibecoded?

- is the formal verification tooling enough?

- what am i overlooking?

I'm aware cybersecurity has countless nuances and formal verification is a small fraction of what it takes to create something secure and reliable.

IMPORTANT DISCLAIMER: While the project is aiming to provide a secure experience, it's far from finished. It cannot be audited or reviewed because it's close-source. I'm sharing here for feedback and demo purposes only. Feel free to reach out for clarity on any of the details instead of diving into the documentation. Pease use responsibly.

I maintain SMRFORGE, an open-source (MIT) tool that seals simulation results into evidence bundles and ships a standalone offline verifier. The verifier re-implements RFC 8032 Ed25519 verification in the Python standard library with its own field arithmetic. I know the advice against rolling your own. That is why I am asking people who do this for a living to try to break it.

Each bundle section (inputs, result, provenance) is canonicalized and hashed with SHA-256. The section digests roll up into bundle_sha256, which is SHA-256 of the canonical digest list. The signature is over the ASCII string "sha256:<hex>" rather than the raw 32 bytes. The verifier first checks the signature under the public key embedded in the bundle. That is the integrity verdict. It then compares the embedded key to a pinned key as a separate origin verdict. So the verifier does process arbitrary keys, which is why the input rules below matter.

Decisions I want reviewed

1. Cofactorless and strict. It checks [s]B == R + [k]A exactly, with k = SHA-512(R || A || M) read little-endian. There is no cofactor multiply.
   
2. It rejects a point encoding with y >= p, a scalar s >= L, and any point not on the curve.
   
3. It rejects small-order points where [8]A or [8]R is the identity. It also rejects a recovered x == 0 with the sign bit set, per RFC 8032 section 5.1.3 step 4.

This intentionally differs from libsodium, which is cofactored, and from original ref10, which is permissive, on small-order and mixed-order inputs. The right reference is a cofactorless strict verifier such as ed25519-dalek verify_strict, or the strict profile in Chalkias, Garillot, and Nikolaenko, "Taming the Many EdDSAs." The challenge is to find a (public key, message, signature) where my accept/reject disagrees with that profile.

About testing. There are 24 in-tree vectors, but the verifier itself produced their expected outcomes. They are regression and self-consistency checks, not independent known-answer tests. The independent checks were cross-validation against OpenSSL on random keys and messages in both directions, and the Chalkias et al. speccheck vectors. Every copy was run against those during development, but they are not vendored in the repo. There are five copies of the verifier, four in Python that largely mirror each other and one separate JavaScript implementation in the browser checker.

Known weaknesses. The RFC 3161 timestamp token is only shape-checked offline (valid base64 and a leading DER SEQUENCE tag). A separate openssl tool verifies it against a pinned TSA CA. And this is hand-rolled Ed25519 in pure Python.

My questions. Is rolling section digests into one signed bundle_sha256 sound? Should the trust-critical path use a vetted library, with the stdlib code kept only as a cross-check? Is shape-checking the timestamp offline and deferring crypto verification to openssl an acceptable split?

AI disclosure. I used Claude to write most of the verifier and to check this post against the source. I used Grok to draft and tidy the post. The prompts are in a comment below.

Sources

- Verifier: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/smrf_verify/verify.py#L450
- Vectors: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/conformance/ed25519/small_order_vectors.json
- Generator: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/tools/gen_ed25519_kat.py
- RFC 8032: https://www.rfc-editor.org/rfc/rfc8032#section-5.1.7
- Taming the Many EdDSAs: https://eprint.iacr.org/2020/1244
- ed25519-dalek verify_strict: https://docs.rs/ed25519-dalek/latest/ed25519_dalek/struct.VerifyingKey.html#method.verify_strict

Not the first, will not be the last

A lovely & broad lay-person discussion of the OpenAI Navier-Stokes story and LLMs in mathematics.

We'd hopefully by now all know that hosted LLMs companies train upon their customers uploads and sessions (). It's clear this *"surveillance plagiarism" is a threat to cryptographers and security researchers who do really original work, as well as to any corporation using AI, but open weights models address this threat.

Vi Hart touches upon a broader array of topics: LLM psychosis. Modern mathematics was always a machine to be applied, ala the phrase "tenure machine", so AI doing so makes some sense. LLM proofs could retard the development of important abstractions, like how Aschbacher's announcement of the CFSG slowed research on the CFSG.

It stays solidly focused upon mathematics research however, without much direct discussion of applied topics like cryptography. Yet, there are fairly obvious impacts upon cryptography.

We correctly assume LLMs should overall raise our confidence in cryptographic software, because of auto-formalisation, eventually someone should figure out how to make LLMs write SE Linux profiles, etc and these are by far the lions share of the attack vectors.

Yet conversely, if LLM proofs cause mathematical subfields to be abandoned, then overall our confidence in problems being hard could decline, because organisations like IDA-CCR or China's version might not abandon some subtly relevant subfield. In other words, hybrid PQC+ECC protocols should become more important because of LLMs, not less.

Scott Aaronson also has an excellent post about LLM usage in mathematics too, somewhat more targeted towards mathematicians and computer scientists. It's slightly weakened towards the end by giving credence to AI doomer drama, but that's easily ignored.

Around (*), you should expect hosted LLM compajies would train upon data they promise not to train upon, either now or in future. In particular, there is a rich literature of non-cryptographic privacy preserving machine learning techniques, so similar work would buys them plausible deniability when training upon restricted data, but such techniques typically wind up being broken eventually.

Aside: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs 

I'm the developer of SMS Import / Export, an Android Kotlin app that sequentially writes and reads large (multi GiB) files. A few months ago, I decided to add encryption to the app. I assumed that this would be a simple matter of finding an appropriate library / API that implemented the recommended modern standards, something in the AES or ChaCha20 families, and wiring it up.

Then I realized that I really should use authenticated encryption, and that's where the headaches began. Java / Kotlin offers CryptoOutputStream and CryptoInputStream, which can be used with AES-GCM or ChaChaPoly20-Poly1305 for authenticated encryption, so I initially tried them - but soon realized that they don't do streaming authenticated encryption and only authenticate the input stream after reading all of it, which means that I need to either buffer multiple GiBs of decrypted data in memory - not feasible on Android devices; store the decrypted data somewhere on disk - obviously insecure, or have my app process not-yet-authenticated data - obviously a bad idea.

I looked around for a ready-made streaming authenticated encryption solution, but the only one I could find was Google Tink's Streaming AEAD primitive. I tried using it, but I found Tink frustrating to work with, in large part due to its highly opinionated insistence on the use of its key management abstractions and its push toward the use of centralized key management systems.

So I wound up writing my own high level streaming authenticated wrapper around the libsodium SecretStream API, which I eventually split off into its own library, SecretStream For Kotlin:

Internally, SecretStreamOutputStream accumulates data passed in write() calls in a fixed size buffer; whenever this buffer fills up, the data is passed to the SecretStream API for encryption and the result is then written to the underlying OutputStream. (When the stream is closed, any remaining data is written in a final chunk, which may be smaller than the standard chunk size.) SecretStreamInputStream reads data in fixed size chunks, each of which is passed to the SecretStream API for decryption and authentication and the result stored in a fixed size buffer, from where it is provided to read() calls. No data is returned until it has been authenticated.

I'm not a cryptographer, and I was really hoping to find a ready-made solution and avoid reinventing any wheels or rolling my own crypto.

Questions: Is my approach sensible? Is there a better approach? Did I miss any useful facilities or libraries that I should have been using?

and part 3 !

previously:
part 2 https://00f.net/2026/10/06/zeroization-2/

part 1 https://00f.net/2026/10/06/zeroization-1/

Internxt is a post-quantum secure encrypted cloud storage provider which is open-source and has passed multiple independent audits.

I reviewed their code and found that post-quantum security should have been the least of their problems. Clicking a link in your browser could trigger remote code execution on the desktop app or leak your long-term encryption keys to an attacker-chosen URL. Their cryptographic architecture stands on shaky grounds with public keys never being verified, in some cases man-in-the-middled by design, a flat key hierarchy and a KDF with just 3 iterations of MD5.

We need PQC and we need it now, but adding a (self-rolled) PQC hybrid on top of a weak protocol does not make it more secure.

> LLM Disclosure: I used an LLM to help me write this post along with many hours of work, some of the findings (i.e. the RCE) were found with a local Qwen 3.5 27B model inside opencode (thanks r/LocalLLaMA ). It is impossible to share a single prompt since it was an iterative process, but I'm happy to elaborate on my methods if anyone cares.

Hi guys, I wrote an open source enigma machine game. I was wondering if any experts in this could give me some feedback, tell me if it's accurate or anything I missed, and also give me any suggestions on how to make it more fun. Thank you.

Cloudflare says about two thirds of the human traffic on their network is already PQ. Google put a 2029 date on finishing their migration. Every PQ readiness writeup this month leads with those two numbers like the job's mostly done.

I think the numbers are real and the framing is backwards. TLS was the easy part. Three companies control the browser and the edge, kyber is cheap, nobody had to change their behaviour, so it happened. Good. But look at what "harvest now, decrypt later" actually threatens. It's not the TLS session you'll open tomorrow. It's the ten years of sessions someone's already recorded, and no migration on earth un-records those. That damage is done and it's weird how rarely anyone says so out loud.

Then look at where the long-lived secrets actually live. Disk encryption keys wrapped with RSA on a TPM. Backups encrypted to an ECC key from 2018. SSH keys. Every code signing and firmware signing chain on the planet, which is signatures, which is the part of PQ that's still ugly (dilithium sigs are 2.4 KB, sphincs is worse, and a lot of boot ROMs can't hold either). Messaging got PQ key exchange but most of it still authenticates with classical signatures. None of that is at 65%. Most of it's at zero and has no date.

So the migration that got done is the one that was easy to measure, and the migration that matters is the one nobody can measure, so it isn't on anyone's slide.

Where I'm probably wrong: maybe TLS first is right because it's where the volume is, and volume is what a harvest attack feeds on. And maybe signatures genuinely don't need to move until there's an actual machine, since you can't forge a signature retroactively the way you can decrypt a recording. That second one I half believe. But "we'll do signatures when the quantum computer exists" means every device with a burned-in classical root key is stuck trusting a forgeable signer the day it exists, and nobody's re-flashing a billion boot ROMs in a hurry.

Am I underrating what's actually been done outside TLS? Is anyone here doing a real at-rest or signing migration and not just the handshake? And is there a good argument that the harvest-now problem was already lost before 2024, so we should stop pretending the 2029 dates fix it?