Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory | AIChainDay