Trusted Execution Environments (TEEs), also known as secure enclaves, such as Intel SGX, Intel TDX or AMD SEV are seeing widespread use to perform computations on highly sensitive data. To analyze the security of cryptographic protocols using TEEs, several formal models exist, notably the one by Pass et al. (EUROCRYPT 2017) for attested computations in the Generalized UC framework. Using this model and the proposed global ideal functionality , provably secure multi-party computations with practical efficiency are possible. Attested computations are achieved by having enclave outputs signed with a key pair held by , together with the enclave's code. Being a global functionality, the verification key can be obtained by any party. Perhaps surprisingly, this model does not give rise to a meaningful notion of public verifiability, i. e. the ability of external parties to plausibly verify results, even though some commercially available enclaves allow exactly that. We formalize this intuition in the form of an impossibility result and propose a novel simulation technique where equivocation is not handled by the simulator resp. adversary anymore, but in a coordinated effort between our new functionality and a (local) ideal functionality that is realized with public verifiability. To this end, several technical problems need to be solved, in particular to ensure that this new mechanism cannot be abused. While unconventional, this approach is, to the best of our knowledge, the first to achieve a general variant of public verifiability a) even when all protocol parties are corrupted and is probabilistic and b) where guarantees of honest (external) verifiers are not affected by simulation at all. We call the latter property global public verifiability. We also address a second impossibility result of Pass et al., namely the requirement that every protocol party needs a TEE (even in a setting without public verifiability), unless an additional (global) setup is used. We address this impossibility result by introducing designated-verifier attestations that are only valid for a single party in a single protocol execution, akin to what is possible with real-world enclaves. Using our improved model, we propose protocols for (globally publicly verifiable) composable general MPC and prove their security under the notion of Universal Composition with Global Subroutines (Badertscher et al., TCC 2020) and static malicious corruptions.