This document is an overview of how the software in the Plutus project is structured. Most things are in direct subdirectories of the root, so we will work through those in conceptual order.
Plutus Core is the language that actually goes on the blockchain. Consequently this is the absolute core of the codebase, and everything depends on it. It also includes the Plutus IR intermediary language.
Plutus Tx is how we refer to the subset of Haskell which we compile into Plutus Core. This is how users actually write Plutus contracts: they write Haskell programs, part of which is compiled into Plutus Core. The rest of the program can then use this compiled code when submitting transactions.
We have done a fair amount of work in specifying and formalizing parts of our system. At the moment all of this work also lives in the Plutus repository, and we even have some basic testing of the Haskell implementation against the Agda formalization.