Agenda How can we split the efforts to write a spec for the solving algorithm in quint. What do we need from Taiga? set up one working group on:quint specs taiga FHE hacking Collaboration on the solver blockchain as suggested by Shoaib.

The most important requirement from our side is a better technical understanding of how the whole system works and is secured. The working should be clear from the mockup when it's completed, but it incorporates no security features. What kind of circuits are to be built in addition to those already existing in Taiga? A better understanding or walkthrough of Taiga's API and codebase would be really helpful. Also, the codebase of Taiga gives errors when I try to import it to a REPL environment for Rust like evcxr. It would be nice to rectify that. A formal specification seems like a good idea, because there is a privacy gap when solvers can actually see the intents during solving. A spec would make incrementally changing the protocol (e.g. with the goal of integrating MPC or FHE) easier while still being able to verify correctness. Solver Nodes How does one go about making a solver network? Discussing with the Informal Collaborative Finance team, we thought of potentially using SUAVEs framework a la Anoma. As far as I understand, SUAVE is trying to decentralize block builders by creating a "marketplace" where builders can compete to build blocks using 'user preferences'. What we were discussing was to bring this model to the solvers in an intent centric way. The mapping of SUAVE <> Anoma would look like ->

Collaborative zkSNARKs A solution for verifiable multiparty computation What's the problem? use data that is held by many parties not reveal any more data to each party than what they already have compute securely over this data produce a proof of correct computation and output 1, 2 and 3 together constitute classical multiparty computation.

Verifying hyperproperties with TLA Preliminaries A behavior is a sequence of states. A step is a pair of consecutive states. A state machine is a behavior model which is described by an initial predicate $\mathcal{I}$ and a next-state predicate $\mathcal{N}$.