2026-05-31 · testnet · pqc-networking · kms · bridge · zk
The CRITICAL and HIGH testnet-blocking items in PROBLEMS.md are checked off: hybrid ML-KEM + X25519 node transport, a decentralized seal-kms-sidecar (local authority + ephemeral workers, Shamir-split key), single-call bridge withdraw-and-claim with a real Solana/Stellar relayer binary (cursor persistence + Prometheus metrics), seal_submitProof + a consensus-wired ZK verifier, conviction-voting balance checks, RLS CREATE POLICY DDL, and operator runbooks (node-failure recovery, backup/restore, QUICKSTART, drain-before-migrate bridge lifecycle). The biggest remaining piece is the proof backend — the ZK path still defaults to a StubVerifier, so proofs aren't verified end-to-end yet, and a security pass is ongoing. "Close to testnet," not "testnet is live." If you'd run a validator, partner on the bridge, build a SQL dapp, or review the crypto, now's the time to get in touch.
2026-04-21 · ringtail · bridges · demo-apps · adr-001
Field note on the week between the 2026-04-13 public-mirror sync and now. Most of the following is in the private tree; a batched public push is coming once the bridge e2e scripts stop finding their own bugs.
- Full Ringtail protocol path (Lagrange coefficients + canonical rounding), replacing the
SimpleThreshold signature-list stand-in — the 2-round aggregate shape from ePrint 2024/1113.
seal-ringtail-verify: no_std verifier that compiles for Solana BPF and Stellar Soroban; feature-gated on both bridges. Compute-unit projections in place for the BPF side.
- Real Solana/Stellar observer RPC clients; Anchor + Soroban programs for committee-MAC verify; real SAC transfers on Stellar; a
docker-compose + bridge-e2e.sh that drives a bridged-asset round-trip locally.
- Per-chain bridge emergency pause with a 2/3 Technical Council supermajority gate;
seal_getBridgeStatus surfaces paused_chains.
TxType::DexMatch emitted per block, so matched trades land in the state root and ZK proof rather than only in the engine's in-memory book.
- ADR-001: SQL stored procedures (CALL / PL/pgSQL-shaped) as the default contract model, WASM as an opt-in path with
wasm-validate at deploy.
- Four demo apps under
apps/: copy-trading.seal, kyc.seal, kindle.seal, forms.seal (MPC + ZK + AEAD + browser wallet end-to-end).
- Kani 66/66 (the last 6 closed by a BTreeMap swap + harness refactor); test count 820 → 887 over the week.
2026-04-12 · architecture · consensus · sql
Against the current tree, crate by crate — what's wired, what's a placeholder with a TODO header, and what's honestly aspirational. Corrections vs. an earlier draft: production sortition is ML-DSA + SHA3 (not "Algorand VRF"); SimpleThreshold is a signature-list stand-in and RingtailThreshold is the real one; the DEX is a per-block batch auction with Lean-proved matching invariants. Bridges are TLA+-proved on the invariants but not yet production-validated end-to-end against a live Solana / Stellar validator.
2026-04-05 · formal-methods · lean · rocq · tla+
Counted against the current formal/ tree: TLA+ (3 specs + 2 model-check drivers; SealConsensus covers Agreement / NoEquivocation / MonotonicHeight / Progress on 2/3-threshold voting; SealBridge maps MintedLeqLocked, NoDoubleMint, NoMintWithoutLock, BurnedLeqMinted to concrete checks in bridge.rs). Lean 4 with an Aeneas MIR-extraction pipeline on seal-merkle, plus hand-written proofs for Hash, VRF (LaV), and DEX matching — 29 theorems. Rocq modules for Balance, StateMachine, SqlState, RLS — 29 theorems. 66 Kani harnesses across 19 files. 9 cargo-fuzz targets. Miri is a soft skip in CI today, which is a known gap.
2026-04-12 · pqc · ml-kem · secure-memory
Adjacent project, same stack. ML-KEM-768 (FIPS 203) is wired as a standalone primitive in rust-secure-memory — 1184-byte public keys, 1088-byte ciphertexts, 32-byte shared secrets. Important correction over an earlier draft: Enclave sealing is symmetric-only (XChaCha20-Poly1305 with a per-process session key), and ML-KEM is not currently in the sealing path. Three Kani harnesses plus a cargo-fuzz target cover input validation and the FIPS 203 implicit-rejection behaviour; neither proves anything about ML-KEM's underlying MLWE/MLWR soundness.
More posts (FPGA meta-compiler, Thetis26 wait-free, Monte Carlo GPU, concurrent C++ verification, ARIA strategy DSL, market-data terminal, LOB reconstruction on GPU, tabular embedding, QML build pipeline, etc.) at zeta1999.github.io/renoir42.