I build reinforcement-learning environments and tools for formal reasoning.

Code RL beyond sampled tests: models complete C functions under fixed specifications and earn reward from Frama-C proofs of functional correctness and runtime safety. The public release includes 64 tasks, an isolated judge, negative controls, and reproducible proof evidence.

Math RL without hidden answer keys: prompts and Lean checks come from the same bounded specification, while models submit ordinary answers or complete finite certificates.

The verifier behind MathCheck RL turns bounded specifications and candidate answers into Lean programs, checks the complete finite domain in isolation, and records exactly what each verdict means.

Across 640 samples per condition, grammar masking moved Qwen first-line CFG acceptance from 65.6% to 100% and familiar tactic starts from 60.2% to 91.3%—without claiming Lean correctness.

An audit of a Lean tactic grammar using executable counterexamples, extraction analysis, and 6,413 mutation and prose probes—separating corpus fit from actual constraint strength.

Can feature entanglement be shaped during model training, not only decomposed afterward? Across ten seeds in overcomplete toy networks, an L2+GELU configuration showed 17.9% lower SAE-measured interference than L1+ReLU.

An early Phi-3-mini experiment that uses circuit analysis to localize one factual association, suppress it with IA³, and then learn a counterfactual replacement; the code preserves the full experimental pipeline.

An early-layer LoRA method for propagating Swahili–English lexical alignment already present inside Lugha-Llama toward its output representations, evaluated on 623 training pairs and 63 unseen controls.