The signature check in your pocket — verifying Betrusted's ed25519
Betrusted's Precursor is what happens when someone takes "trust nothing you can't inspect" seriously all the way down: open silicon on an FPGA, open OS (Xous), open enclosure, and a threat model that assumes the supply chain is out to get you. I've admired the project for years, and its xous-core tree is worth reading purely as systems literature.
Here's the thing though: a device like that concentrates its trust brutally. Signed OS updates, signed gateware, signed loader — the entire integrity story of the machine funnels through ed25519 signature verification, running on the device's own fork of curve25519-dalek (v4.1.2, adapted for Xous and the Precursor's constraints). Audit the silicon all you want; if the verify routine's arithmetic is wrong, the funnel accepts what it shouldn't and everything above it is theater.
So the fourth target of the verification family is exactly that fork: pinned snapshot in betrusted-curve25519-dalek-source, its own Charon/Aeneas extraction, and the full pyramid proven in Lean 4 about the extracted code — field 𝔽ₚ (p = 2²⁵⁵ − 19) at the real limb weights, the complete twisted-Edwards group law, Scalar52 mod ℓ, and at the apex the EdDSA acceptance criterion: the extracted verifier accepts iff compress([s]B − [k]A) matches the signature's R. Axiom cone audited by the build; SHA-512 and wire formats are the only opaque boundary, enumerated by name.
Of the three forks in the family, this one is the purest expression of why fork-by-fork verification matters. Solana's fork guards value transfer; RISC Zero's guards proofs; Betrusted's guards a device whose whole reason to exist is verifiable trust. Its users chose it because they want the assurance chain to bottom out somewhere inspectable. Machine-checked correctness of the signature core is what "inspectable" looks like when you stop meaning "someone could theoretically read the code" and start meaning "a kernel checked every step of the argument."
Same rules as the siblings: theorems about the transpiled Rust, never a re-model; status table backed by verification/check.sh; deferred work (point-level lifting, verified decompress) stated openly. Four targets, one method, and after this campaign I trust the method enough to say the per-target marginal cost is now dominated by the fork's actual semantic drift — which is exactly the quantity you want to be paying for.