From AI slop to formal verification: Changing how we do bug bounties as AI takes over

Starting next month, Nym is beginning our code freeze in preparation for its next annual security audit. We are rolling out post-quantum cryptography throughout the network and apps, as well as new cover traffic schemes, and so a new security audit is in order. Every year we put our apps and code through an independent review to make sure we are delivering the privacy and security promises we make to the people who use the network.

After this audit, we're going further toward formal verification. Currently, AI models such as Claude Fable make it easier to find attacks, and we’re finding that our current bug bounty program is mostly attracting “AI slop” as a result of people trying to run AI security audits against our code.

At Nym, we have started running Claude Fable against our code on a continual basis in order to discover real bugs. Similar to the ZCash Ironwood upgrade, the only way to guarantee our code against possible bugs that can be discovered by AI is via formally verifying each primitive and protocol used by Nym.

Bug bounty program: What’s changing

In preparation for our next security audit and the paradigm shift towards formal verification, we are stopping our bug bounty program in its current form.

This means discontinuing the payout system we've run to date in which $NYM tokens were paid out on a fixed scale, tiered by the severity of the issue reported. Nym will now pay only on a discretionary basis for severe and important findings. We are still accepting reports, and researchers can and should keep sending us anything they find. Our safe haven policy and responsible disclosure rules still stay in place.

The current guidelines are always up to date at nym.com/vdp-bbp.

Why we're doing this

Nym’s code is open source and independently reviewed every year, rather than taken on trust.

What's different this time is the method. This upcoming audit, run with an external security firm, needs for us to freeze the code-base before the audit begins, which is why we're pausing the bounty rewards now. In the end, a bug bounty program and a deep audit cover overlapping ground, and reports that are already caught by an audit in progress don't add much. Concentrating our security effort on the audit and then formal verification is the better use of resources.

Next stop: Formal verification

After this audit, we are moving with our partners at Cryspen towards formal verification. Where a bug bounty and a conventional audit look for flaws by testing and review, formal verification generates mathematical proofs of code behavior to show that critical parts of a system behave exactly as intended, and cannot do certain things at all. It is the highest standard of assurance in security engineering, and it is where privacy infrastructure like ours should be heading.

Of course, until recently this has been too time-consuming to do over a large codebase like Nym, but AI tools now make large-scale formal verification possible for the core cryptographic primitives and protocols of Nym.

To learn more about formal verification, read A Roadmap for High Assurance Cryptography written by our CEO Harry Halpin, while he was at Inria de Paris in 2017 working with Karthik Bhargavan, who led the formal verification of protocols (like TLS 1.3 and Signal) on which the entire internet depends. With Karthk Bhargavan now at Cryspen, we’ll be working with his team on formally verifying Nym’s core cryptography and protocols.

Our audits so far

Nym and NymVPN have been independently audited and reviewed by leading firms and cryptographers since the early days of the network. The record is public in our Trust Center:

• Cure53 (July 2024). A broad audit of Nym's mobile and desktop apps, the VPN, network infrastructure, and cryptography, carried out by a team including Dr. Daniel Bleichenbacher. See the Cure53 audit.

• Oak Security (January 2023). Two audits: one of the Nym mixnet and vesting contract, and one of the Nym wallet.

• Dr. JP Aumasson (September 2021). An early security review of the network by one of the field's best-known cryptographers.

• Cryspen technical reviews (2023–2024). Cryptographic reviews of Nym's distributed key generation and the Outfox packet format, led by Dr. Karthikeyan Bhargavan and colleagues, using formal methods.

That last item matters here: formal, mathematical review is not new to Nym. This next audit extends that approach across more of the system.

What this means for you

For users, nothing changes except that our security process is getting stronger. Your NymVPN and the network keep running as normal.

For security researchers, the door stays open. If you find a vulnerability, report it to security@nym.com, ideally encrypted with our PGP key, with clear steps to reproduce.

Rewards are now discretionary, reserved for severe and important findings, but every credible report still gets acknowledged, still gets fixed, and still helps protect everyone who uses Nym. Full instructions are on the vulnerability disclosure page.