The no-C, pure-Rust project reached one of the harder corners of computing this week — formal methods and computer algebra — and a whole cluster grew around it at once. z3rs is a from-scratch port of the Z3 theorem prover; puremp is the arbitrary-precision numeric core it stands on; latticefoundry is an LLVM-shaped compiler that uses z3rs to superoptimize; and mathesis is a browser math notebook that surfaces both. Separately, puregit implemented git — client and server — in pure Rust.

z3rs: a pure-Rust Z3

z3rs is "a pure-Rust, no_std port of the Z3 theorem prover, free of any third-party or native dependency." It reimplements Z3 (pinned at v4.17.0) as a single crate with no GMP, no C, no -sys crate — its only dependency is puremp. Z3 is an SMT solver: it decides whether logical formulas over theories (integers, reals, bit-vectors, arrays, floating-point, …) are satisfiable, and it sits under symbolic execution, program verifiers, and constraint solvers across the industry.

The week moved through whole theory fragments:

• Floating-point (QF_FP) — the common fragment decides, by bit-blasting symbolic operations to bit-vectors: fp.mul, fp.div, fp.sqrt, fp.fma, fp.roundToIntegral, and to_fp conversions, each a port of Z3's construction, bit-exact across formats.
• Nonlinear real arithmetic (QF_NRA) — decided via CAD (cylindrical algebraic decomposition), with a Bareiss determinant / resultant chain and a cofactor-expansion fallback.
• Horn clauses / CHC (Phase G) — single- and multi-predicate constrained Horn clauses, deciding acyclic systems exactly in both directions and declining cyclic ones fast — the shape program verifiers pose their problems in.

puremp: the numeric core

puremp is "pure-Rust, clean-room arbitrary-precision arithmetic" — integers, rationals, MPFR-class floats, decimals, complex, polynomials, matrices, intervals, and algebraic numbers, no_std. It's the GMP / MPFR replacement z3rs needs, and it's grown into a small computer-algebra system in its own right. The week spanned the whole tower:

• Factorization — Pollard rho and ECM in the Montgomery domain, plus SIQS (self-initializing quadratic sieve) with a single-large-prime variation.
• Polynomials — Cantor–Zassenhaus factorization over finite fields GF(q), Newton fast division, Half-GCD, Kronecker multiply.
• Linear algebra — division-free determinant and characteristic polynomial over any ring (Berkowitz), exact rational-matrix eigenvalues, Strassen–Winograd multiply.
• A generic algebraic layer — Ring and Field traits so Poly and Matrix work over ModInt, GF(pᵏ), or any ring, plus elliptic curves y² = x³ + ax + b over GF(p) and ℚ.
• Transcendentals — AGM (Brent–Salamin) ln, digamma / polygamma, beta, and Bessel functions.

latticefoundry: an LLVM, and it uses the solver

latticefoundry is "a clean-room compiler-construction framework in pure Rust" — roughly the role LLVM plays, built independently: a typed SSA IR, a verifier, a pass pipeline, target-independent codegen, a machine-code / object-file layer, and a linker core. The week was remarkable in how far it went: an x86-64 target (SysV ABI, instruction selection, a real machine-code encoder), then a second AArch64 target to prove retargetability, a .lf linker that produces a running native executable, an -O optimization pipeline with cross-module LTO, DWARF debug info (lf build -g), and — the tie back to the cluster — an in-process JIT with z3rs superoptimization and a "certified" tier emitting proof-carrying refinement certificates. It also grew lf-cc, a clean-room C frontend (full preprocessor, aggregates, switch/goto, function pointers) compiling C to LatticeFoundry IR.

mathesis: a notebook on the whole thing

mathesis is "a Mathematica-style computational notebook that runs entirely in your browser" — type a Wolfram-style expression and get an exact answer, computed client-side with no server round-trip. It's a Vue 3 notebook UI wrapping a Rust math engine compiled to WebAssembly, and the engine is a straight frontend to this week's foundations: puremp for the arithmetic (elliptic curves, Gamma / Bessel, arbitrary precision) and z3rs for the solving (SatisfiableQ, its dual TautologyQ, a visual Solve builder). The week added session variables, cryptographically-secure RNGs, autocomplete with signature help, and (* … *) comments. It's live on GitHub Pages — the human-facing end of the z3rs / puremp stack.

puregit: git, client and server

puregit is a pure-Rust implementation of git in the spirit of libgit2 — the object model, packfiles, references, the index, and the smart transfer protocol, as both client and server, over HTTP and SSH, on purecrypto for object hashing. The week (80 commits) took it deep: delta-compressed pack writing, thin packs on push and fetch, side-band-64k multiplexing for upload-pack, an SSH upload-pack entry point and a post-receive hook on the server, lockfile-based ref updates, commit-graph and multi-pack-index formats, SHA-256 object-format negotiation, linked worktrees, and reflog expiry. It's the version-control layer of the same no-C toolchain.

erigon-seg: Ethereum state files

erigon-seg reads, queries, writes, and merges Erigon 3 seg state files (.kv / .bt / .kvei) in pure Rust — the on-disk format Erigon uses for Ethereum historical state. It reached v1.0.1: a reader verified against real Erigon files, then the write side (seg pattern compression, the .bt writer in both layouts, the .kvei bloom writer), k-way domain merge, and a KvStack multi-file surface.

Also this week

• kataan kept grinding test262 — iterator helpers, generators, duplicate-named regex groups, and freeze/seal on function and Date cells — another ~100 commits shaving the known-failure ledger down.
• graphitesql held its hundred-commit pace on the SQLite engine.
• decryptd — a GPU worker for a distributed-compute project: pulls work chunks, runs them on an NVIDIA GPU, reports NVML temperature / power / throughput in a tray (now via ldtray), ships as a RunPod-friendly container.
• rsupd — signed release distribution and in-place auto-update for Rust programs (the successor to goupd), where a program trusts an update from nothing but a 32-byte fingerprint baked into it.
• TibaneApp + libwallet — a wallet recovery/backup redesign: desynced-2FA-share repair, reliable reshare-ceremony timeouts, and a Help & FAQ screen.
• oxideav-vc2 (SMPTE VC-2) and oxideav-ape (Monkey's Audio) — two more clean-room codecs.

Next week

z3rs widens the decided fragments toward the full SMT-LIB theory set; puremp keeps filling in the CAS surface beneath it; latticefoundry and mathesis lean harder on both. puregit closes its protocol gaps. And the systems layer from last week — pebbledb, graphitesql, httpsd, usbmagic — keeps maturing at its steady pace.