The research record is the methodology.

Introduces a hierarchical consensus protocol that achieves scalability by being optimistic, operating fast when conditions are favourable, while relaxing liveness to a weak form under adversarial conditions. Formalises handover and justifiability properties and proves safety and liveness for blockchain and distributed systems settings.

Presents Hooks, a modular checkpointing protocol for Nakamoto-style blockchains. A hook is a forward-pointing digital signature from a block to one of its descendants, the forward analogue of a parent hash link. A quorum of hooks forms a checkpoint, enabling trustless bootstrap via public verifiability. Unlike prior protocols, Hooks does not solve an agreement problem; it extends the input chain's safety guarantees while requiring only weak safety, converting unsatisfied safety requirements into liveness issues.

Uses CSP to formalise assemblies of distributed agents (including blockchain nodes) operating as consensus machines, sequential state machines that achieve predictable outcomes despite Byzantine agents communicating via message passing.

Applies formal CSP modelling and verification to blockchain consensus, addressing the problem of ensuring that decentralisation cannot allow two valid decisions to arise simultaneously. Models a primary consensus mechanism supplemented by a backup triggered when the primary is blocked.

Proposes a protocol combining two TEE technologies: an SGX enclave acts as a trusted guest owner to deploy, attest, and provision AMD SEV VMs, bringing SGX-style flexible remote attestation to SEV. Formally verified with the Tamarin prover; demonstrated on accountable ML models.

Introduces the notion of an orderly SGX enclave, splitting enclave behaviour into execution phases, each enforcing a policy over accesses to untrusted memory, phase transitions, and register sanitisation. Implements Guardian, an open-source tool using symbolic execution (via angr) to automatically validate whether an enclave binary is orderly and to detect typical enclave attack primitives. Distinct from vulnerability-pattern tools like TeeRex: Guardian checks structural policy adherence rather than searching for known exploit patterns.

Develops a protocol for program certification where neither the producer nor an external body needs to be fully trusted. Using encrypted sources inside a TEE, TCPA allows all parties to trust delivered object code without the producer ever releasing unencrypted source to any external entity.