The IMR program seeks to develop automated tools that protect modern electronic markets from adversaries exploiting public interfaces to cause disruption or economic damage. It combines LLM-based automation with formal modeling and analysis to create machine-analyzable market models from informal descriptions, identify hidden weaknesses, and formulate “resilience conjectures.” The program will analyze these conjectures to prove resilience or generate concrete counterexamples, then use them to recommend and confirm repairs to market designs. This capability is intended to protect U.S. markets and the civilian and military critical resources that depend on them, addressing gaps in current legal and regulatory protections focused on profit-seeking manipulation.