Midgard

This is an unfinished project where the goal was to formally verify Midgard. Midgard is the first optimistic-rollups L2 for Cardano.

Main ideas:

• State machines as computational inductive relations (i.e. there is at least a computable function that realizes them).
• Local (to each machine) properties as analyzing reachable states.
• Rules to combine different machines keeping them computable. Parallel and simultaneous (product) composition plus a way to restrict their interfaces.
• Rules to define properties on combined machines, normal inductive properties over reachable states.
• Property based testing with Plausible.
• SMT and Model checking with Blaster.