Trust
Evidence you can check yourself.
Webfold is built so that a security reviewer does not have to take our word for it. This is what is proved, what is measured, what is recorded, and what we are still building.
Assurance
Four layers, each checkable.
Proved core
The arithmetic at the centre of the engine's data structures (the apeiron library) is proved in Lean 4 from the Rust that runs, extracted with Charon and Aeneas, with no `sorry` and an audited axiom list. Webfold's own kernels are proved the same way: page-template counting and thresholds, the hidden-content decision, acquisition budgets and text shaping: 149 declarations with zero axioms, audited before the latest merges and not re-run on them. The BigInt kernels (limb arithmetic, division, parse and format) are proved too, with Lean's three core axioms. The proofs cover these kernels, not the whole program, and the proved surface grows each release.
Private by construction →
Conversion, the browser engine and redaction run in one process on your machine. There is no browser farm and no third-party model in the request path. Outbound requests pass an address guard that refuses private and metadata addresses.
Evidence by default →
Capture any fetch as a standard web archive with the exact bytes. Claims in a research report carry their source and a content hash. Two captures can be diffed to show exactly what changed. Desktop takeovers are logged.
Measured with the protocol shown →
Every number on this site comes from a result file with its harness, dataset and date. The harness repository opens with the public release. Critical guarantees have mutation tests: break the code and the gate must go red. Where we lose a comparison, the page says so.
Published now.
Coming.
Status page
Uptime for the hosted API and this site.
Trust centre
Policies, sub-processors and security documents, published as they exist.
Compliance
We will say nothing about SOC 2 or similar until an audit is complete.