Independent AI researcher working on post-training with reinforcement learning, RL environments, and formal verification.
Instead of rewarding C code for passing a test suite, Formally Verified C rewards a model only when Frama-C proves that its implementation satisfies a fixed ACSL specification, including runtime-safety obligations. The public alpha includes 64 tasks, an isolated judge, adversarial negative controls, and reproducible proof evidence. Technical article.
An RL environment for mathematical reasoning that does not rely on hidden answer keys. Models return an answer or a complete finite certificate, and a frozen problem specification with a Lean-backed checker determines the reward. Technical article.
The verification engine behind MathCheck RL. It turns bounded mathematical specifications into Lean checks for exact answers and complete finite relations, returns explicit failure reasons, and can evaluate untrusted model output in isolation. Technical article.
- Grammars for AI Proof Steps — two articles and reproducible experiments on grammar-guided Lean tactic generation.
- Taming Incidental Polysemanticity in Toy Models — a research note on training choices and feature-entanglement proxies in toy networks.
- Targeted Lexical Injection — early-layer LoRA experiments for Swahili–English lexical alignment.
- Surgical Knowledge Rewrite in Compact LLMs — an early exploratory study of circuit-localized, two-stage IA³ knowledge editing.
These preprints are part of my earlier research; my present work centers on RL environments and formal verification.
I publish research notes and technical essays at stanleyngugi.netlify.app.
Research questions, criticism, and collaboration proposals are welcome through the contact links on my website.