Tech Stack

Cairo - a Turing-Complete Programming Language
In order to prove the validity of a computation in a STARK proof, it must be expressed in algebraic form. Cairo is a CPU architecture, decoupling the business logic, which can now be written in a high-level programming language from the algebraic representation that can be efficiently proven by STARK. This way, developers can focus on writing the desired business logic, without the need to understand and account for translating it to efficient mathematical representations. Cairo is a modern programming language reminiscent of Rust. Cairo makes it easy to develop, test, and maintain contract logic without the need to deep dive into the STARK algebra.
StarkWare defines the Cairo-Architecture and implements it both as a native VM, and as a proving-optimized algebraic form. StarkWare develops additional developer tools around the Cairo programming language, such as compilers from higher-level languages, debugger, IDE support, and more.
The Cairo toolchain is developed in Rust for great flexibility, performance, developer experience, and readability.

Starknet: A Decentralized ZK-Rollup
Starknet is a permissionless decentralized ZK-Rollup operating as an L2 network over Ethereum. StarkNet solves the blockchain scalability problem by enabling significantly higher network throughput, thus also lower cost per transaction while leveraging Ethereum’s security. Developers can write Starknet contracts using the Cairo language and deploy them on the network, and users can send transactions to these contracts (in a similar manner to Ethereum).
The two main components running Starknet are the Sequencer (which generates blocks, similar to miners in Bitcoin or validators in Ethereum) and the Full Node (that syncs on the state of the network). Both are built in Rust, to enable both safety and good performance. This optimizes the proving performance of each transaction execution. A Solidity contract deployed on Ethereum connects the Starknet network (L2) to Ethereum (L1).
The Starknet transaction execution environment, called Starknet OS (similar to the Ethereum Virtual Machine), is implemented in Cairo.
The Starknet Prover is optimized for performance by implementing C++ and some low-level assembly. It runs over micro-services architecture in the cloud.
The Verifier is implemented in Solidity, allowing proofs to be verified on the Ethereum blockchain.

StarkEx: Managed Services
StarkWare runs separate instances of its L2 appchain (an L2 system providing scale on top of Ethereum) for premium customers. Such services do the heavy lifting of communicating with the Blockchain and the Application smart contract (over Starknet or Ethereum), to apply off-chain logic as required, and expose an application-specific API, allowing the customers to focus on their core competence. The off-chain services are implemented in Python using and typically implement a cloud micro-services architecture.