Yeah! Tortä

DNSCrypt, DoH and ODoH client for Android - no root ad blocker, DNS privacy, encrypted DNS resolver with a local CDN, Rust engine, Slint UI and Lean 4 proofs.

Most privacy tools on Android tell you they are working. A switch turns green, a card says protected, a counter goes up. Almost none of them can tell you whether a single query was actually answered the way the card claims — and the gap between "armed" and "working" is where privacy software quietly fails.

Yeah! Tortä is an Android DNS engine built around the opposite instinct. Every pillar has to produce evidence a user can read: a ledger row, a counter that moves, a resolved address you can ping. When a pillar cannot prove it is working, it is designed to go dark rather than look green — because a feature that silently drops your connections is worse than a feature that is off.

🦀 Rust core — resolver, forwarder, blocklist, mirror, warden. #[cfg]-gated, no root required. 🎨 Slint UI — the whole interface is compiled Rust, not XML layouts. 📐 Lean 4 proofs — the invariants that must hold for every input are machine-checked, not sampled. 📓 A ledger you can read — cache/query.log, one tab-separated row per decision, with the gate that made it. It began as a fork of InviZible Pro (AGPL-3.0) and has grown a Rust engine, a Slint interface, a content-addressed local CDN and a formal-methods layer around it.

🎯 Mission — Give people a privacy tool that can show its work: every protection backed by evidence they can read for themselves, and every limitation stated as plainly as every strength.

🌟 Vision — A world where "this app protects you" is a claim with an instrument behind it, not a marketing line — and where saying "this part is not proven yet" is normal engineering rather than an embarrassment.

Built by Nova-Violet Role, a non-profit working at the intersection of law, code and cognitive science. Everything we make is open, free, and meant to be taken apart.

🏛️ The nine pillars Each pillar is a distinct guarantee with its own code, its own counters and its own failure mode.

1. 🛡️ WARDEN — the datapath gate rust/torta_core/src/warden/ · 10,087 lines

The last thing between a packet and the network. Warden holds numbered rules (block_dns_bypass, hardcoded-resolver denial, port policy) and decides whether a connection — not just a name — is allowed to exist. It is the pillar that catches an app trying to talk to 8.8.8.8:53 directly, having never asked us to resolve anything.

2. 🌌 CENTAURI — the offline CDN rust/torta_core/src/mirror/ · 24,407 lines · #[cfg(feature = "mirror")]

A Decentraleyes/LocalCDN idea taken further: a content-addressed, signature-verified local mirror. Common CDN assets (jQuery and friends) are fetched at most once, hash-verified against a minisign-signed catalog, and served from a loopback server afterwards. The upstream CDN sees one request ever, instead of one per site you visit.

It is guarded by a four-conjunct gate — TLS trust and something servable and a watched host and that exact host in the servable set — because an interception that cannot serve is a black hole, not a privacy win. That gate is proven in Lean (CloakServable.lean), and the reason it needs all four conjuncts is written into the source as an incident report.

3. 🎭 MASKSOLVER — the resolution ladder rust/torta_core/src/resolver/ · query-masksolver.log

Escalates a query through transports until something honest answers: cache → local records → DNSCrypt → DoH → plain, with retry budgets, negative caching, TTL floors and ceilings, and serve-stale. Every rung records why it moved to the next one, so a slow answer can be attributed instead of guessed at.

4. 🐺 BEAST — the adaptive tuner rust/torta_core/src/beast/ · 8,364 lines

Watches live behaviour (latency, loss, cache hit rate) and tunes the engine's own knobs — window, in-flight cap, pacing. The interesting engineering is the anti-thrash work: hysteresis and invariants that stop a tuner from oscillating between two equally bad states, which is the classic way self-tuning systems make things worse.

5. 🔄 ROTATION — the upstream carousel RotationManager.kt + engine pool/routing

Rotates DNS upstreams on a schedule so no single operator sees your whole history. The load-bearing part is the health gate: after switching, it sends real labelled queries (torta-rotverify-<entropy>.example.com) and rolls back if the new upstream does not answer. Reachable is not answering — that lesson is now formalised in RotationAnsweringGate.lean, and it recurs across the codebase.

6. 🍰 WIRE CAKE INU — privileged capability, without root libumdnscrypt/src/main/kotlin/.../wire_cake_inu/

Self-ADB elevation and a catalogue of what that unlocks (PowerCatalogue.kt). Where a capability genuinely needs more privilege than an app has, this pillar acquires it explicitly and reversibly, and reports what it gained — rather than pretending the feature works without it.

7. 🔐 DNSCRYPT — encrypted transport rust/torta_core/src/resolver/dnscrypt.rs + ResolverRuntime.kt

DNSCrypt v2 and DoH, with post-quantum-capable exchanges counted separately from classic ones (pq_exchanges / classic_exchanges) so you can see what you are actually getting, not what was negotiated in theory.

8. 🕳️ UNDERGROUND LAYER — the deny plane rust/torta_core/src/resolver/underground.rs

Blocklists, homograph detection, rebind protection and the DoH-bypass sinkhole. Every denial is attributed to exactly one of five labels — blocklist, warden, underground, homograph, doh-bypass — and that labelling is proved injective in DenyAttribution.lean, so two different gates can never be confused in the ledger.

The doh-bypass label exists because of a measurement that invalidated everything else: a fully-rendered browser page produced zero ledger rows. The browser had resolved its own DoH endpoint once and tunnelled every subsequent lookup to Cloudflare, blinding all nine pillars at once. Sinkholing the bootstrap apexes is what restored visibility — the ledger now shows brave.cloudflare-dns.com … REJECT … doh-bypass.

9. 🌐 NETSTACK FORWARDER — the tun datapath rust/torta_core/src/forwarder/ · 3,686 lines

The userspace network stack behind the VPN interface: TCP/UDP forwarding, SNI inspection, and the hairpin that lets a cloaked CDN host reach the local mirror. No root, no kernel module.