Crash-tested AI-agent transactions. Attack-tested Wi-Fi security.

Tested designs and their evidence, to license or acquire, for teams building AI-agent platforms and Wi-Fi equipment: agents now change real files and databases, and quantum-safe signatures no longer fit in one Wi-Fi frame.

Read the results License or acquire a result Try the Verifier

Illustration

29/29: Chosen mid-write crash points, each recovered cleanly
3: Leaking tool combinations found; pair-by-pair checks miss two
64 KiB: Modelled access-point memory ceiling; without our quota, none holds
0/755: Attack probes accepted by our multi-link Wi-Fi rule; a naive rule accepts all

Two results on AI agents

Each has its own page, with the method and the evidence.

AI agents · crash recovery
29/29Chosen crash points, each recovered cleanly
Crash tests on an AI agent’s changes
At every crash point we chose, the agent layer recovered cleanly. Tests at random kill moments are reported on its result page.
Read the result
AI agents · tool safety
3Smallest tool sets that leak a stored secret
Safe in pairs, unsafe as a set of three
In a ten-tool test on real files and a real database, two are triples whose every pair is safe within our three-call search.
Read the result

Crash tests on an AI agent’s changes, compared with: How SQLite Is Tested, section Crash Testing. Retrieved 2026-10-06. The lab's test uses the method SQLite documents: kill a process in the middle of a write, recover, and check that the change either completed or was rolled back. SQLite's testing also simulates power loss, which this result does not. Retrieval record.

More results

More results, on code patches, chip netlists, network standards, Wi‑Fi sign-in and permissions, each on its own page

Explained in plain English

All results and their evidence · All posts

Platform

One practice in two fields: test what breaks, and prove what can be proved.

AI agents

We kill our agent transaction layer on purpose and measure how it recovers, and we search combinations of agent tools for sets that are unsafe together.

Why now: Assistants are now given the power to change real files and databases, and platforms let users combine tools from different sources (Simon Willison on why that is risky). Transaction layers for agents, such as SagaLLM and Cordon, are recent research; we did not find crash-under-kill measurements in either.
For: Agent-platform, runtime-security and diligence teams deciding which layer to trust and which tools an assistant may combine.

Post-quantum Wi‑Fi and networks

Quantum-safe signatures and some keys are too large for one Wi-Fi frame, so an access point must hold half-finished sign-ins in memory. We prove a memory ceiling for a modelled access point and publish chip-design files and C code for a receiver with bounded memory.

Why now: The US standards body has published its first quantum-safe key-exchange standard (NIST FIPS 203).
For: Wi-Fi, Ethernet, chip and network-equipment makers, and teams auditing a quantum-safe library.
Also: Deterministic Ethernet. A proved minimum for how much a redundant-path receiver (IEEE 802.1CB) must remember when it must be able to recall, for every frame still in its window, which path delivered the first copy: for a two-frame window, more than the standard's duplicate-dropping bitmap holds, under one reading of the standard.
Retransmissions on a link. A computed floor on how many resend rounds a modelled radio link needs, with our own resend rule measured against it.
Claim diligence. We run the standard's own test vectors against third-party code and publish what reproduces and what does not.

Nick Harris, founder. CTO of VivaMed BioPharma; co-founder of MedSim.ai, FastRead.io and Formulai.

Check our work yourself

Drop a file you downloaded from this site, and your browser checks it is the one we published. Nothing is sent anywhere.

Checker · runs in this tab

$ Drop one of our published files anywhere on this panel.

or try

Theorems & Bounds

Our results for Wi-Fi and network equipment, each a formula with its scope in plain words. The full statements, their limits and the rest of the results are on their own page.

Measured search
$# {attacks tried} = 8 rounds \times 1400 = 11200, # {attacks that got through} = 0$
$# {attacks tried} = 8 rounds \times 1400 = 11200,$ $# {attacks that got through} = 0$
11,200 attacks on our models, none got through
An attack search on our modelled Wi-Fi sign-in designs found no way through within its budget, and caught a known flaw we re-opened on purpose.
The full statement and its limits
Checked by the Lean 4 kernel
$\forall σ \in Ev^{*} : mem_{AP} (run_{G, c} (σ)) \leq G = 64 KiB (c = 16 KiB, N_{m a x} = 4);$ $\forall B \exists σ : mem_{AP} (run_{c}^{no quota} (σ)) > B$
$\forall σ \in Ev^{*} : mem_{AP} (run_{G, c} (σ)) \leq G = 64 KiB$ $(c = 16 KiB, N_{m a x} = 4);$ $\forall B \exists σ : mem_{AP} (run_{c}^{no quota} (σ)) > B$
The access-point memory ceiling
In our modelled access point, no attacker schedule pushes pre-authentication memory past the ceiling; without the quota, any budget can be broken.
The full statement and its limits Its result page
Sessions, any numberWith the quotaWithout it
Proven ceiling
Uncapped
The memory ceiling, in a model of the admission module: with the access-point quota it holds for any number of sessions; without it, any budget can be broken. Bar lengths are drawn, not measured.

The standard's own test cases, run on the library we build on

Run against the open-source liboqs library, NIST's own test cases give 255 pass, 60 not exercised, because the library offers no way to run those. For the signature algorithm only key generation is checked, not signing or verifying. This checks a library we did not write; it is not one of our own results.

The full statement and its limits

All theorems and bounds, including the Lean-checked floor for redundant-path Ethernet receivers

Artifacts & Open Source

21open repositories, datasets and live demos.

All open repositories, datasets and demos

Intellectual Property

We have drafted patent claims for designs for quantum-safe Wi-Fi sign-in, handover and redundant-path Ethernet. Each was examined in software models, with one or more of proofs, model checking, replayed known attacks and simulator runs; the tools differ by area, and no hardware has run them.

How each area was checked

Where we are

No customer, no revenue, no pilot, no third-party audit.

The access-point memory ceiling is proven for our model of the admission-control module; it is not yet enforced inside a production access-point program or on real Wi-Fi frames.
Our hardware designs are checked with the open-source Yosys tool and in simulation, and every run was on Apple computers; no router, switch or access-point chip has run our code.
The 11,200-attack search ran on a fixed budget: zero escapes is a null result, not a proof that none exist.
Every check is our own: Lean 4, Z3, TLC, Yosys and NIST's test vectors for the network work, and private test code and checkers for the AI-agent results.
The code behind these results is private. Where a file holds that code, we publish its fingerprint instead, under this label: Withheld: the bytes are not published; the digest is. A digest is that fingerprint: hash a copy of the file and compare it with the one listed on the published-files page.
No patent has been granted and no standard-essentiality opinion has been obtained.