Clazel

A web browser built from the bottom up by AI, using formal verification instead of trust.

• Memory safe: 100% safe Rust except clazel-sys: 14 unsafe blocks (20 lines) that enter the OS sandbox, machine-checked and audited.
• Verified where it matters: the kernel's security policy and every parser of untrusted input carry machine-checked proofs (Verus, Kani).
• Honest about it: each crate declares its verification tier, and the trusted computing base is listed in docs/VERIFICATION.md.

Status: Phases 0 (foundations) and 1 (verified primitives) are complete: UTF-8 (clazel-encoding), percent-encoding (clazel-percent), forgiving base64 (clazel-base64), MIME types and sniffing (clazel-mime), IDNA (clazel-idna) and URLs (clazel-url) are at Tier 2, on macOS and on Linux CI. Phase 2 (kernel and IPC) is in progress; see the table below and docs/phases/phase-2.md. Phase 3 (networking) has HTTP field syntax, HTTP/1.1 response framing and request serialization (clazel-http), DNS (clazel-dns) and the request builder (clazel-fetch) implemented at tier 0, target tier 2, and a minimal curl clone: clazel fetch URL does one http:// GET through our own resolver and the proven URL parser, request builder and response parser, and prints the response. It has no TLS, redirects or cookies yet. The TLS work (DER, RSA PKCS#1 v1.5 verification and TLS 1.3 message formats) is parked on the phase3/tls branch until it passes CI. Full CI verification is pending; the remaining networking work is in docs/phases/phase-3.md. Recheck every proof yourself, on Linux x86-64, with:

docker build --platform linux/amd64 -t clazel-verify .
docker run --rm --platform linux/amd64 clazel-verify

See docs/ROADMAP.md.

Verification status

CI rewrites the table below on main after every push whose full verification passes. Until that first happens it predates Phase 3: it has no rows for the Phase 3 crates, which stay at tier 0.

Crate	Tier (target)	Verus	Kani	Axioms	unsafe blocks (lines)⁵	Lines: spec / proof / exec¹	Spec mutations: theorem / incidental / survived²	Conformance⁴	Spec review³
clazel	0 (0)	not used	no harnesses	0	0 (0)	—	—	WPT cookies/ domCookieTest, document.cookie set and get through real processes: 11 / 11 WPT cookies/ httpCookieTest, document.cookie read through real processes: 166 / 167 (1 expected failures)	no spec files
clazel-base64	2 (2)	80 verified, 0 errors	no harnesses	0	0 (0)	665 / 758 / 173	23 / 0 / 0 of 23	WPT fetch/data-urls base64: 80 / 80	0 of 3 files current
clazel-cookie	2 (2)	424 verified, 0 errors	no harnesses	0	0 (0)	4066 / 4061 / 1676	43 / 0 / 0 of 43	WPT cookies/ httpCookieTest and domCookieTest tables: 177 / 178 (1 expected failures) cookie_store differential, random set and get sequences: 3000 / 3000 http-state dates/: 70 / 70 http-state parser corpus: 195 / 222 (27 expected failures)	0 of 9 files current
clazel-dns	2 (2)	242 verified, 0 errors	no harnesses	0	0 (0)	1979 / 1668 / 869	163 / 0 / 0 of 163	captured DNS responses: 12 / 12 hand-built DNS messages: 24 / 24 resolv.conf nameserver lines: 10 / 10 simple-dns differential: mutated messages: 58731 / 60000 (1269 expected failures) simple-dns differential: our queries: 4000 / 4000 simple-dns differential: random messages: 8000 / 8000	0 of 5 files current
clazel-encoding	2 (2)	81 verified, 0 errors	no harnesses	0	0 (0)	764 / 485 / 205	22 / 0 / 0 of 22	WPT encoding/ UTF-8 decode: 57 / 57 WPT encoding/ UTF-8 encode (decode cases reversed): 8 / 8	0 of 3 files current
clazel-fetch	0 (2)	164 verified, 0 errors	no harnesses	0	0 (0)	1500 / 1108 / 595	64 / 0 / 0 of 64	http-state parser corpus (through the client): 195 / 222 (27 expected failures) url and cookie_store differential, random redirect chains: 1500 / 1500	0 of 5 files current
clazel-http	2 (2)	407 verified, 0 errors	no harnesses	0	0 (0)	3364 / 3188 / 1734	150 / 0 / 0 of 150	RFC 9112 7.1 and 11 examples: 122 / 122 framing by construction: random bodies: 3000 / 3000 httparse differential: handcrafted heads: 29 / 44 (15 expected failures) httparse differential: llhttp corpus heads: 124 / 136 (12 expected failures) httparse differential: mutated responses: 53915 / 60000 (6085 expected failures) httparse differential: random responses: 6000 / 6000 llhttp test/response and framing cases: 109 / 136 (27 expected failures)	0 of 5 files current
clazel-idna	2 (2)	375 verified, 0 errors	no harnesses	0	0 (0)	2406 / 2887 / 17549	69 / 0 / 0 of 69	RFC 3492 section 7.1 samples: 19 / 19 WPT url/ IdnaTestV2.json: 2675 / 2675 WPT url/ toascii.json: 87 / 87	0 of 5 files current
clazel-ipc	2 (2)	177 verified, 0 errors	no harnesses	0	0 (0)	1240 / 1076 / 545	69 / 0 / 0 of 69	RFC 8949 Appendix A (cbor/test-vectors): 82 / 82 minicbor differential: random and mutated bytes: 60000 / 60000 minicbor differential: random items: 20000 / 20000	0 of 7 files current
clazel-kernel	2 (2)	340 verified, 0 errors	no harnesses	0	0 (0)	3229 / 4264 / 1103	36 / 0 / 0 of 36	WPT cookies/ domCookieTest tables, document.cookie set and get through the kernel: 11 / 11 WPT cookies/ httpCookieTest tables, document.cookie read through the kernel: 166 / 167 (1 expected failures) WPT url/ urltestdata.json navigation (rows with a base): 336 / 336 WPT url/ urltestdata.json origin_of and path_of (rows without a base): 560 / 560 WPT webstorage/ localStorage calls: 24 / 24 cookie_store differential, random multi-renderer document.cookie traces: 3000 / 3000 scalar and ASCII guards never fire (WPT urltestdata.json and fuzz): 2896 / 2896	0 of 3 files current
clazel-mime	2 (2)	288 verified, 0 errors	no harnesses	0	0 (0)	2584 / 2122 / 1640	35 / 0 / 0 of 35	WPT mimesniff/media: 6 / 7 (1 expected failures) WPT mimesniff/mime-types: 955 / 955 WPT mimesniff/sniffing feeds: 2 / 2 WPT mimesniff/sniffing mislabeled binary: 3 / 3	0 of 5 files current
clazel-net	0 (0)	not used	no harnesses	0	0 (0)	—	—	none	no spec files
clazel-origin	2 (2)	43 verified, 0 errors	no harnesses	0	0 (0)	495 / 209 / 284	31 / 0 / 0 of 31	HTML 7.1.1 example tables (same origin, same site): 11 / 11 WPT url/ urltestdata.json origin: 414 / 414 differential vs rust-url Url::origin(): 403 / 414 (11 expected failures)	0 of 3 files current
clazel-percent	2 (2)	54 verified, 0 errors	no harnesses	0	0 (0)	520 / 297 / 173	34 / 0 / 0 of 34	WPT url/ percent-encoding: 23 / 32 (9 expected failures)	0 of 3 files current
clazel-psl	2 (2)	201 verified, 0 errors	no harnesses	0	0 (0)	1063 / 1840 / 45824	23 / 0 / 0 of 23	differential vs publicsuffix 2.3.0: 49685 / 49685 publicsuffix tests.txt checkPublicSuffix: 78 / 78	0 of 3 files current
clazel-renderer	0 (0)	not used	no harnesses	0	0 (0)	—	—	none	no spec files
clazel-sandbox	1 (1)	not used	8 successfully verified harnesses, 0 failures, 8 total	0	0 (0)	—	—	none	no spec files
clazel-sys	0 (0)	not used	no harnesses	0	14 (20)	—	—	none	no spec files
clazel-url	2 (2)	565 verified, 0 errors	no harnesses	0	0 (0)	5725 / 5260 / 2026	144 / 0 / 0 of 144	WPT url/ setters_tests.json: 278 / 278 WPT url/ toascii.json: 87 / 87 WPT url/ urltestdata.json: 896 / 896 WPT url/ urltestdata.json hosts: 359 / 359	0 of 7 files current
xtask	0 (0)	not used	no harnesses	0	0 (0)	—	—	none	no spec files

¹ From Verus's line_count; only code inside verus! is counted, and type definitions count as exec. ² Only the first number is coverage: a proven theorem is false for that many deliberately broken specs. See docs/VERIFICATION.md. ³ Optional human reviews of specs, contracts, axioms and mutation labels, unchanged since review. They gate nothing; see docs/SPEC-REVIEWS.md. ⁴ Measured by the run: passing / total units per vendored suite, as each tests/conformance*.rs reports them. Expected failures are counted separately and never as passes. See docs/VERIFICATION.md. ⁵ Counted by cargo xtask check: unsafe blocks (and unsafe extern blocks), with the lines from the unsafe keyword to the closing brace. Only clazel-sys may have any; the rule and its audits are in docs/VERIFICATION.md and docs/SYS-AUDITS.md. ⁶ The host shell (crates/clazel/src, item 2.15) is 298 lines, counted as wc -l counts them over its Rust files; the plan's limit is 300. The command line and the demo (crates/clazel/cli, item 2.16) are not counted: they only call the shell's public functions.

Phase 2 process tests: where they have run. The demo (cargo run -p clazel -- demo), the sandbox escape attempts, the hostile-renderer test and the WPT cookies/ run through real processes (item 2.16) have been run on macOS arm64 only, locally: macOS is not in CI. On Linux they have never run (they were written on a Mac), and CI on ubuntu-24.04 cannot run them until a maintainer decides how to allow unprivileged user namespaces for the renderer, which otherwise fails closed (see item 2.16 in docs/phases/phase-2.md). Attempts to fork and to ptrace a sibling are not made yet: they need a clazel-sys addition and its audit. The table has rows for clazel and clazel-renderer once CI next updates it.

Formalizing the standards has already found one spec bug: see docs/ERRATA.md.

Building

scripts/setup.sh         # install the pinned, checksummed toolchain (needs rustup)
scripts/verify.sh        # every check, fresh proof runs (same as `cargo xtask verify`; CI runs this)
cargo xtask verify --changed   # every check, but proofs and tests only for crates changed since origin/main
cargo xtask check        # fast static checks only

The command-line browser, clazel, and the sandboxed renderer it starts for each tab:

cargo build --release --bin clazel --bin clazel-renderer   # both land in target/release/
target/release/clazel fetch http://example.com/           # one http:// GET, response printed

fetch resolves the host with our own DNS client, sends a request built by proven code, and frames the response with the proven HTTP/1.1 parser. It needs the Internet, and speaks only http:// for now.

Each GitHub release has a Linux x86-64 tarball with both binaries and an installer: unpack it and run sudo ./install.sh (or PREFIX=... ./install.sh). On Ubuntu 23.10 and later, which restrict unprivileged user namespaces, the installer also adds an AppArmor profile that lets clazel-renderer create the one its sandbox needs, and nothing else; without it the renderer refuses to start, by design. Built from source, run the same script once:

sudo packaging/apparmor/allow-userns.sh clazel-renderer "$PWD/target/release/clazel-renderer"

How to get involved

The code is written by AI agents under rules (CLAUDE.md) designed so that nobody has to trust them. That leaves a lot of useful work for people, and much of it is work only a person can do.

• Check our work. Rerun every proof on your own machine with the Docker command above, or scripts/verify.sh. If anything does not match the verification status table, open an issue: a claim nobody can reproduce is a bug.
• Review a spec against its standard. Each spec.rs transcribes a standard step by step, with its modelling choices listed at the top (docs/SPEC-STYLE.md). Reviews gate nothing, and only people may record one, so a reviewed file means a person read it. See docs/SPEC-REVIEWS.md for how. contract.rs files are the shortest route to what each crate actually promises.
• Take errata upstream. Formalising the standards has found places where they are wrong as written. Agents never file issues with standards bodies; the entries marked "Reported upstream: not yet" in docs/ERRATA.md are waiting for a person to check them and report them.
• Try to break it. Feed the parsers hostile input, look for a spec bug the proofs would not catch (each crate's mutations.json lists the known gaps, marked survives), or close one of those gaps with a lemma or a Kani harness.
• Add test suites. Every Tier 2 crate is tested against official suites and independent engines (tests/conformance*.rs). Point us at suites we have not vendored, or at engines worth differential testing against.
• Run it where we have not. The Phase 2 process tests (the sandbox, the hostile renderer) have only run on macOS arm64, and never on Linux. The README says why under the status table.
• Read clazel-sys. It is the only crate with unsafe: 14 blocks that enter the OS sandbox. Every change is audited by a second model (docs/SYS-AUDITS.md); a person reading it too is welcome.
• Build the next phases. The plan is in docs/ROADMAP.md and the detailed plans in docs/phases/. TLS is parked on the phase3/tls branch until it passes CI. Contributions go through the same machine checks as everything else, whoever (or whatever) wrote them: read CLAUDE.md first, and expect cargo xtask verify --changed and CI's full verification to be the bar.

License

MIT. See LICENSE.