Ptyhon is the language we will use to create the program, the glue that will connect everything. Not only is the Pluspy library that we will be modifying written in Python, but it is an easy language to create wrappers for the NVMe client that we will be interfacing with.

TLA+ (Temporal Logic of Actions) is a specification language that allows its users to formally specify the logic and behavior of a system or design, focusing on temporal or concurrent reasoning. We will center everything around this language when creating test cases and validation.

The PlusPy library interprets TLA+ specifications for Python. Pluspy will allow us to use the power of Python and programming on top of a language that can only formally specify design and modeling.

NVME-CLI is a Linux tool for interacting with NVMe-compliant interfaces. It issues low-level commands directly to the NVMe SSD controller, which might not be accessible otherwise through regular use.

We will use a Linux distro to use NVMe-CLI properly and have the least restrictions on hardware interaction. We chose Ubuntu for its ease of use and support, which also allows us to build and use the NVMe-CLI.

Visual Studio Code is an integrated development environment owned by Microsoft. VSCode will be our team's primary IDE as it has an extensive extension library and supports multiple languages. Its ease of use and versatility will be vital to the project's success.