This page contains links to TLA+ specifications that accompany the paper Verifying Hyperproperties with TLA by Leslie Lamport and Fred B. Schneider. That paper describes two toy systems Tiny and Little and how TLA is used to verify that they satisfy the hyperproperty called GNI. These descriptions are formalized in the following TLA+ modules. Modules Tiny and Little specify the two systems, and modules TinyGNI and LittleGNI contain their verifications, which consist of a combination of TLAPS checked proofs and TLC checked properties. The source files and pdf files of their pretty-printed versions are contained in a zip file that can be downloaded by clicking here.