Renoir42

Lock-free/wait-free data structures, formally verified

Post-quantum L1 with native SQL. PHP+MySQL, but on-chain.

GPU-accelerated HFT backtester with Aria language for fast strategy development

Real-time market data terminal, PQ encrypted

FPGA meta-compiler: from DSL to silicon with formal proofs. 10 backends (Verilog, VHDL, CUDA, Metal, Lean 4)

Secure memory: guard pages, mlock, encrypted enclaves, post-quantum KEM

Experiments with the formalization of numerical algorithms

Iris-style concurrent separation logic, mechanized in Lean 4: fancy updates, world satisfaction, invariants — proved sorry-free.

A harness for building tools with local models: a ReAct agent loop with world-model lookahead, and distillation of large agent models into small local students (1B / 3B / 8B). Built to drive leanlift and the security toolkit. Closed source; the public repo is the shareware surface.

Storage on machines you do not trust. The peer holds ciphertext: transit-only, passphrase, or end-to-end.

Post-quantum TLS and SSH demos. Hybrid X25519 + ML-KEM-768, with classical auth where that still has to interoperate.

Agents for security. A scanner orchestrator (SAST / DAST / SCA / secrets) with LLM-assisted triage and agent-assisted pen-testing over a SARIF + DuckDB store. Companion to Seal DAO.

A crypto-exchange emulator with a real matching engine. Binance- and Coinbase-compatible APIs, for testing trading and OMS systems.

Simple, composable Rust libraries for building agent tooling fast from a harness: TUI widgets, networking, a capability-scoped shell, secrets, remoting, and a sandbox.