typhon icon indicating copy to clipboard operation
typhon copied to clipboard

Published 20 hours ago • verified publisher icon anoma

Execution Engine Formal Spec

Open isheff opened this issue 1 year ago • 0 comments

Develop a formal specification for the execution engine in TLA+ or similar. This will involve some kind of assumptions about the Taiga API. Ideally this would match up with the formal Heterogeneous Paxos Spec and formal Heterogeneous Narwhal Spec, so we can formalize how they work together.

Prerequisite

  • [ ] https://github.com/anoma/specs/issues/123

Sub-Tasks

  • [ ] Formal description of Execution Engine
  • [ ] Serializability Proof

isheff avatar Mar 29 '23 22:03 isheff