Isaac Sheff

Using the [Heterogeneous Paxos](https://arxiv.org/abs/2011.08253) [Spec developed earlier](https://github.com/heliaxdev/hpaxos/issues/2), can we formalize and prove heterogeneous termination in [Ivy](http://microsoft.github.io/ivy/) or [TLA+](https://lamport.azurewebsites.net/tla/tla.html)?

Using our [multi-chain nodes](https://github.com/heliaxdev/dist-sys-pm/issues/1), enable cheap creation of additional chains with the same quorums as a "main chain." This would allow transactions with the same integrity as the main chain...

Implement a [programming model](https://anoma.network/blog/heterogeneous-paxos-and-multi-chain-atomic-commits#programming-model) for atomic message passing between [state machines running on a Heterogeneous Paxos Chain](https://github.com/heliaxdev/dist-sys-pm/issues/8). This can be based on [IBC](https://ibcprotocol.org/), bug should provide additional atomicity guarantees. Note...

On a [Heterogeneous Paxos chain](https://github.com/heliaxdev/dist-sys-pm/issues/6), run a state machine for each "main chain," such that blocks can contain bundles of transactions on multiple chains. Note that: - Not all nodes...

Ultimately, we want our existing ledger node / consensus participants to be able to support multiple chains within the same program, rather than as totally separate, unrelated processes. Specifically, we...