A while back I wrote up simple tools as an umbrella for a few Rust libraries I kept reaching for — a TUI layer, a networking layer, a capability-scoped shell. It’s worth saying out loud what the umbrella is actually for, because that’s what decides where it goes next.

leanlift is an effort to mechanize Iris-style concurrent separation logic in Lean 4 — the program logic you reach for when you want to actually prove things about concurrent, resourceful code rather than argue about them. This week a milestone closed: Phase A2, the fancy-update layer, is complete and sorry-free.

“Le Harnais” is a harness for building tools with local models — the agent loop, the CLI (lh), and the plumbing that lets a small model do useful work. Two pieces landed recently that are worth writing down, because they go together.

Two public example repos are up — flow-master-examples and price-master-examples — showing how to actually consume the Quant Masters products. Both ship under a clear licensing model: each product is available binary-only or with full source, and these repos demonstrate the binary-only seam. This post is mostly about Flow Master.

Short version: Seal DAO is approaching a public testnet, and the protocol isn’t frozen yet — what you do on the testnet shapes what mainnet commits to. The architectural blockers are in and tested; what’s left is the kind of work that goes faster with more hands and sharper eyes on it. So if any of this is your thing — running a validator, partnering on the bridge, building a SQL-native dapp, reviewing the cryptography, or backing the project ahead of testnet — now is the time to reach out. The rest of this post is what landed to get here, and what’s honestly still open.

Follow-on to the LU + QR post. That one was about classical linear algebra dual-stacked in Lean 4 and F*. Since then two things landed: a complete machine-checked proof of the Johnson–Lindenstrauss lemma, and the start of a randomized SVD. Worth being precise about which is done and which isn’t.

“simple tools” is an umbrella for three Rust libraries I keep reaching for when building local agents and developer tools: a TUI/widget layer, a networking layer, and a capability-scoped execution layer. Different maturities — worth being precise about which is which.

Early flag: this is a scaffold post. The repo is at “initial commit — appsec CLI scaffold + fixtures + planning docs.” What follows is the shape it’s being built into, not a shipped tool. Purge Master is a companion to Seal DAO — the security program for a post-quantum chain with a lot of Rust and a DEX needs its own toolchain.

This one is a plan, not a release. Trade Master — codename Vivaldi, keeping the composer naming next to Paganini and Sibelius — is the binary that would quote, hedge, route orders, hold inventory, and talk to venues. The pieces around it already exist; the integrating engine is the work in progress.

First, a name collision to clear up. There are two things called Aria in this family. The one in gpu-backtest is a strategy DSL — signals and when ... -> buy/sell rules. The one here, in Sibelius, is a contract / payoff description language. Same naming instinct, different jobs. Sibelius is the sell-side core behind Price Master.

Paganini is the Rust quantlib I use for market making, microstructure, and options dealer flow. Flow Master is the commercial packaging of it — the buy-side half of Quant Masters. This post is about what’s actually in the library, not the product page.

Quick field note on Seal DAO. The public mirror was last synced on 2026-04-13. The week since has had most of its work in the private tree; below is what landed there, with a note on what is and isn’t yet in the public repo. I’ll push the batch after it settles.

Thetis26 is a C/C++ library built around wait-free data structures and a thin event loop on top — targeting Linux (epoll), macOS / BSD (kqueue), DPDK, ESP32 and a couple of FreeRTOS boards. The wait-free label applies to the data-structure primitives (ring buffers, hashmap, skip list, STM), not the event loop itself.

Short update on gpu-backtest-public. The optimizer grew a Monte Carlo scenario mode, FX cross-rate costs landed in the cost model, and the Aria DSL picked up a few opcodes.

Follow-up to the Aria-HDL overview on fpga-meta-compiler-public. Short post on what actually landed since that one. Repo still WIP; so are several of these pieces.

Companion to the Seal DAO formal-verification post. That one covered the formal/ tree. This one covers the crates/ tree — which parts are wired up, which parts are placeholders with a TODO header, and which parts are honestly aspirational. The earlier draft of this post inflated a few of those categories; rewriting against the code.

Follow-on to the rust-secure-memory overview. An earlier draft of this post described the KEM as the mechanism behind Enclave sealing. It isn’t. Rewriting against what kem.rs, enclave.rs, and crypto.rs actually do.

Follow-on to the notbbg terminal post. This one is the feed-adapter layer, described honestly against the code rather than as a sales page.

fpga-meta-compiler-public is an HDL and Rust compiler called Aria-HDL. One .ahdl source, ten backends: Verilog, VHDL, Verilator bundle, SymbiYosys/SVA, Lean 4 proof obligations, CUDA, Metal, OpenCL, a JSON resource report, and an IR dump. Marked WIP in the README and here, honestly.

Follow-on to the Thetis26 overview post. This one is concrete: the models/ tree in the repo is organised as a bug taxonomy (BUG-1 through BUG-13+), each tagged to one or more specs, and it’s a better way to talk about formal methods than abstract “what CBMC is good at” framings.

Follow-on to the gpu-backtest LOB post. This one is about the DSL side — bt-dsl, with Aria programs compiled to a bytecode that the same VM runs on CPU, CUDA, OpenCL, and Metal.

numerical-algorithms is a small, explicitly-WIP experiment: take classical linear-algebra algorithms and verify them in two proof ecosystems side-by-side, instead of picking one.

Seal DAO is a post-quantum L1 in Rust with on-chain SQL. The formal/ tree pulls five tool families against different layers. This post is about that tree, not the chain.

this-is-not-bbg-public is a market-data terminal that aggregates ~17 feeds (CEX, DEX, macro, on-chain, news) into a single Go server and three clients. The name is a joke.

rust-secure-memory-public is a Rust port of Go’s memguard — same LockedBuffer / Enclave shape, with an ML-KEM-768 KEM and a set of Lean4 proofs added. Ships with sedit, a TUI encrypted text editor that exercises the library end-to-end.

gpu-backtest-public is a Rust backtesting engine I’ve been building out for HFT-style strategies. Two commits in, still early, but the shape is there: nine crates, a DSL VM, an LOB engine, a DuckDB data layer, and GPU kernels (CUDA / OpenCL / Metal) for the VM and LOB replay. This post covers what’s actually working and what’s not, against the current tree.

A short post on one of my personal C++20 repos: Thetis26-public.

Some notes on one of the experiments we ran at Anzaetek between 2023 and early 2026 inside the Sqetch fintech platform. The work itself is closed source; here I only describe the setup.

Short project-hygiene note. In December 2025 the QCBM + TimeGAN + regime-detection work that had been living inside the Sqetch fintech platform got moved into its own repo, finance_lab. The QCBM + TimeGAN post covers the technical content; this one is just about why the split.

A repo worth a look: ahmetsbilgin/regime-aware-optimal-quoting, a Birkbeck MSc dissertation on extending Avellaneda-Stoikov to regime switching.

Short note on sqetch-tee-fl (private, Sep 2025). A prototype for federated learning under TEE (Trusted Execution Environment) constraints inside the Sqetch fintech platform.

Note on qml_model_02, private 2025 project (Jul 2025 to early 2026). The interesting part isn’t the classifier — it’s the delivery shape.

Short note on tabular_embedding_01, a 2025 project (May–Oct, private). ~107 R-B commits. The repo does not have a public README; this is the shape from the inside.

Follow-on to the year-one QuetzalcoatlProto post. 2024 was a more focused year on the same codebase — ~1,153 R-B commits from Jan to May 2024, concentrated on portfolio optimisation via QUBO and on getting the API layer production-shaped.

A long overdue note on QuetzalcoatlProto (private, LeifKingston/QuetzalcoatlProto), the quantum R&D codebase at the core of the Anzaetek / Laplace quantum-finance work during 2023. Multi-person project; I’m the majority contributor but Amarou Keita, Antoine Mf, aurel10, Maxime ROP, and Keitamara all committed. My 2023 footprint was ~1,662 commits across May to December.

Short note on Aegis, a small event-logging service I built Jul–Sep 2022 (private repo, under the LaplaceKorea org). ~2 months, ~24 R-B commits. Closed source.

Follow-on to the 2021 SSP post. Feb–Mar 2022 was the OAK-D + RAAS integration phase on the oakd-raas branch of moetsi/Sensor-Stream-Pipe.

A note on C99_and_julia_introduction, a short course repo I put together in Feb–Mar 2021.

Contributions to moetsi/Sensor-Stream-Pipe from Aug to Nov 2021, mostly on the raas branch. SSP is an open-source C++ pipeline for compressing and streaming RGB-D sensor data — Azure Kinect, OAK-D, iOS ARKit — to a remote server. Built on FFmpeg / LibAV + NVCodec.

Short note on Atlas, a 2021 private service I built for bursting quantum-optimisation jobs from a small control plane to AWS Braket (D-Wave and gate-model backends). Jun–Nov 2021, ~59 commits. Closed source.

Short note on the original Thetis (Jul 2020, ~136 commits in one month). This is the direct ancestor of Thetis26 — the 2026 rewrite exists because of what this version got right and what it didn’t.

A note on Sibelius, a multi-asset derivatives pricing library I started in late 2019 and pushed hard through 2020 (~158 commits across the year). Closed source beyond the header examples; this is the shape, not the internals.

Please see @ Teaching Demo This is an ‘advanced’ level extract from a would-be embedded C++ training. If further interested, please do not hesitate to contact renoir42 at yahoo.com

I am currently preparing some ‘demo’ teaching sessions around a few subjects:

• Multithreaded & lock-less C++
• (Kalman) filtering
• Trading strategy backtesting, the technical part, i.e. /not/ the strategies generation process per se
• likely, a few other subjects… later.

Nota bene: this is only a proof of concept at this stage.

Going to @ NVIDIA AI SEOUL 2019 (second day, July 2nd). Keep in touch: renoir42 at yahoo.com.

Please see @ Teaching Demo This is an intermediate level extract from a would-be C++ training. If further interested, please do not hesitate to contact renoir42 at yahoo.com

Dear all, I am currently building this github portfolio. This will mostly cover functional programming and math programming, so a mix of, say, OCaml and C++ as well as other tools.