Machine learning (ML) compilers rely on graph-level transforma- tions to enhance the runtime performance of ML models, typi- cally by applying a series of unverified, complex rewrite rules. The rewrite rules must account for the fact that tensor shapes, layouts and ranks may not be known at compile-time (i.e., tensor properties are determined at runtime – for instance, the sequence length of input texts feed into Large Language models is only available at runtime) which makes verifying them challenging. Moreover, com- pilers must apply rewrites so that they are conditionally applied only when certain constraints on symbolic tensor shapes, layouts, ranks, etc. are satisfied. We propose TensorEgg that enables for- mal verification of rewrites operating on tensors with polymorphic shapes, ranks and layouts, and uses a tensor rewrite system that ap- plies these rules to ML computational graphs to enable compilation of dynamically-shaped tensors.