KAME's lock-free software-transactional-memory core is verified by three complementary methods that together close the gap between an abstract protocol and the shipping binary. At the foundation, GenMC exhaustively model-checks the tagged-pointer atomic_shared_ptr reference-counting primitive under the C/C++ RC11 weak-memory model (18 programs, up to ~1.17M executions), proving every memory_order annotation safe against use-after-free, double-free, and leaks. Above it, TLA+/TLC exhaustively explores all thread interleavings: Layer 1 proves atomic_shared_ptr plus commit primitives memory-safe across tens of millions of states (66.5M at 2 threads) and deliberately shows the bare primitive is NOT livelock-free; Layer 2 proves the multi-phase bundle/unbundle STM protocol for 2- and 3-level trees, static and dynamic, both safe AND livelock-free via Lamport-clock priority arbitration, scaling past 1.1 billion states. A hard-link family of six topologies reproduces and fixes the real-world "30/30 abort" production race. Finally, seven C++ stress tests (~27M iterations, 4-8 threads) run the actual implementation on real hardware to catch compiler-, layout-, and timing-dependent bugs the abstract models cannot. The result: the protocol is mathematically guaranteed and the implementation is empirically hardened, with no daylight between them.