Here’s the details of my analysis using Alloy model checker: Analysing simple vault covenant with Alloy