Formal Cedar Spec integration and incremental proof reuse with Lean-POO, and maintained several vertical exmaples in seucirty field