MMaaS: Security Evidence

Security evidence for MMaaS: validator unit and property tests recorded against a named source revision (below), and red-team runs by Claude, Codex and Kimi models, whose findings we investigate and re-test. The validator's most recent red-team record is from September 12, 2026: it ran on the source revision just before the current validator's, which adds one more condition. The most recent red-team run over the combined path (validator, keeper, backend and page) to reach a verdict was on September 10, 2026, and it returned BLOCK: findings to fix before launch. A combined run against the release deployed on October 1, 2026 follows the launch, and funding new books stays closed until that run returns GREEN. None of this is a guarantee that no vulnerabilities remain.

Recorded validator tests

The September 9, 2026 internal run at contract source revision 44714f46a6d4c1f1296f48c98d55bcc2c7090df1 passed 122 unit tests and five property tests with 1,000 generated cases each. The property additions did not change the production validator or compiled blueprint.

Property	What it checks
Conservation	Generated inventory values cannot fund an unauthorised skim.
Pair preservation	Splitting continuations cannot substitute a different input asset pair.
Rewards and fees	Withdrawn rewards remain conserved and are excluded from the inventory fee basis.
Client exit	The client-authorised path still works with invalid bot price floors.
Fill/reprice sequence	Modeled fill continuations and reprices preserve the tested client exit properties.

Removing the pair-preservation check or reward-fee exclusion caused the corresponding tests to fail in mutation runs. These results show that those tests detect those removed checks. They do not establish coverage of every possible defect.

The fill-sequence properties model fills; they do not execute the separate DEX spend validator. The generated inputs cover the defined model, not every Cardano transaction or a complete interaction between both validators.

The record above is from the internal contract repository. It is an internal test report, not a publicly reproducible formal-proof artifact. The public verifier provides the validator source and ceremony/address verification path.

Bind evidence to the code your book uses

Evidence binds to a generation, and a book keeps the generation its credential hashes. Which one that is, and which unapplied hash identifies it, is stated in GENERATIONS.md beside the source itself, and not here, where a copy would go stale the moment a generation is cut and would then deny a real book's existence.

Applying the nine ceremony parameters derives each book's different credential and addresses. Match those against your funded address using the public verifier; matching a source revision alone is insufficient.

A protection added in a later generation does not appear in an older book merely because source or documentation changed. See Validator generations.

We make no Z3 or other formal-proof claim for the active validator without a reproducible artifact naming the exact validator hash, assumptions, properties proved and verifier command. Unit tests, generated property cases and mutation checks are valuable evidence with their own scope; they are not exhaustive formal proofs.