Lean Games

Source code here: Arbitration Games Proofs.

The idea is to design a language combining authenticated data structures and arbitration games in a single place.

Arbitration games come from the world of Optimistic Rollups; the main idea is to replicate some of what they do, but having formal proofs showing that:

• Honest proposers can always defend their claims and win.
• Honest challengers always win and Losing claims are removed.