lean-pl-verify-v2 is a Lean 4 library that embeds Rust (via LLBC/Charon) and TypeScript into a shared state-error monad (RustM) and a language-independent specification logic (ProgramSpec). The central technical result is a full adequacy theorem for the LLBC interpreter (soundness + completeness), established in 18 kernel-checked theorems. Built on this foundation, the framework provides a ProgramSpec combinator library with 30 metatheory theorems, a LangEmbedding abstraction with a satisfies_congr congruence theorem, and a semanticPreservation meta-theorem instantiated at three languages (Rust LLBC, TypeScript, MiniImp). The artefact comprises 351 kernel-checked theorems across five Rust crates, 14 TypeScript functions, and three language embeddings (0 sorry).