Projects
- Midgard : Formalization of L2 optimistic rollups for Cardano.
- Lean Games : Mechanization of Fraud Proof Arbitration games in Lean4. Digital Twin of players.
- Termina – Programming Language : Termina is a domain-specific language for real-time embedded systems aimed at simplifying their implementation and reducing validation and verification costs.
- Multi Formal Playground : Coq Library implementing Tezos model of computation.
- HLola : Stream Runtime Verification Engine implemented in Haskell borrowing (some) Haskell Data Types as Data Theories.
- QuickFuzz : Arbitrary generation of stuff following Haskell Data Types.
- Modelica : Modular Compiler implementation for Modelica (unfinished).
- klytius : Haskell – GHC parallel programs execution observer.
- EasyCrypt : Computer-Aided Cryptographic Proofs.