Reliable use of neural and neuro-symbolic systems requires more than aggregate accuracy: we need explicit evidence about which behaviors are preserved, which internal mechanisms are causally relevant, and when a computational shortcut is safe. This project develops certified abstractions that turn model executions into compact, checkable evidence. The work combines three connected research directions. First, mechanism atlases construct the coarsest exact causal abstraction of a language model relative to a declared prompt family, intervention language, and set of observations. States that remain indistinguishable under all finite intervention sequences are merged, while failures are retained as concrete distinguishing witnesses and compositionally safe regions. Second, AbsLean applies obligation-aware hybrid certification to Lean proof search. Sound abstract analyses discharge inexpensive tactic obligations, exact Lean replay handles the residual obligations, and a separate checker permits pruning only when the evidence ledger is complete. Third, NAPGuard studies whether causally validated activation features can serve as behavioral contracts for detecting regressions between versions of code language models. Experiments will evaluate the methods on Qwen2.5 and GPT-2 language models, BFS-Prover-V2 and ReProver theorem-proving backbones, IOI-style causal tasks, HumanEval+ and MBPP+ code-generation benchmarks, and Lean benchmarks including miniF2F, PutnamBench, and miniCTX. The evaluation will separate discovery, calibration, and held-out testing; compare against matched non-causal and fixed-policy baselines; and preserve negative and boundary results rather than converting approximate agreement into a certificate. The expected outcome is a unified methodology for producing minimal causal state descriptions, checked proof-search pruning decisions, and causally grounded model-update diagnostics, together with reproducible software and machine-readable evidence artifacts. The project is conducted by doctoral student Xiaolin Liu at KTH Royal Institute of Technology under the supervision of Professor Cyrille Artho.