PyMagic is a library used to write specs/models inspired by model checkers. It can be used to write formal specs and has the benefit to improve LLM-code by reasoning over specs instead of real-world running code.