Automated attack path discovery and formal security verification for Ledger hardware wallets (Nano S, Nano X, Stax). Uses PDDL planning to generate multi-vector attack sequences and Alloy for mathematical specification of security properties like key confidentiality and display integrity.