Milestone 3

Collaborate with the Anza team to verify critical security properties of the P-Token contract, including:

• Token minting
• Burning
• Transfer mechanisms

Address technical blockers identified in our analysis:

• Update Rust version for compatibility with our serialization code.
• Ensure compatibility with stable-mir-json output from their repositories.
• Handle unsafe code in state/mod.rs (4 instances) and processor/mod.rs (complex nested loops + unsafe).
• Investigate Pinocchio dependency footprint and selectively verify its used portions.

Improve the sol-semantics library and symbolic execution engine based on insights from this verification effort.