nano-o

Stellar Development FoundationWashington

Pinned Repositories

Caesar
Language:TLA1 4 10
Distributed-termination-detection
TLA+ formalization of a distributed termination-detection algorithm, including a proof checked with Apalache
Language:HTML6 2 10
IO-Automata
Formalisation of basic IO-Automata theory in Isabelle/HOL
Language:Isabelle2 3 00
Isabelle-Semitopology
Language:HTML1 1 00
ivy-proofs
A repository to collect Ivy proofs of various distributed algorithms
4 2 32
MultiPaxos
MultiPaxos and Disk Paxos in TLA+ and PlusCal
Language:TLA12 2 22
PaxosMadeSimple
A TLA+ formalization of the algorithm described in "Paxos Made Simple"
Language:TLA19 2 02
SCP-Verification
Language:TeX3 3 00
tetrabft-tla
Language:TLA2 1 00
TLA-Library
A TLA+ library of concepts that I used in other developments
Language:TLA5 2 10

nano-o's Repositories

nano-o/PaxosMadeSimple
A TLA+ formalization of the algorithm described in "Paxos Made Simple"
Language:TLA19 2 02
nano-o/Distributed-termination-detection
TLA+ formalization of a distributed termination-detection algorithm, including a proof checked with Apalache
Language:HTML6 2 10
nano-o/tetrabft-tla
Language:TLA2 1 00
nano-o/Isabelle-Semitopology
Language:HTML1 1 00
nano-o/ivy-method-in-isabelle
Language:HTML1 1 00
nano-o/streamlet
Language:TLA1 1 1
nano-o/anonymous-consensus
Language:TLA1 0
nano-o/apalache
APALACHE: symbolic model checker for TLA+
Language:Scala0 0
nano-o/dynamic-participation-supplemental
Language:HTML1 0
nano-o/isabelle-amm
Language:HTML1 0
nano-o/ivy
IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Language:C++1 0
nano-o/ivy-docker
Docker setup for Ivy
Language:Vim Script2 0
nano-o/ivy-multipaxos
nano-o/jekyll-website
Language:HTML1 0
nano-o/learner-graphs
Language:TLA2 0
nano-o/Paxos-Isabelle
A safety proof of Paxos in Isabelle
Language:HTML2 0
nano-o/python-fbas
A tool for reasoning about Federated Byzantine Agreement Systems
Language:Python2 02
nano-o/racket-fbas
Language:Racket1 0
nano-o/racket-wasm
Wasm tooling in Racket.
Language:Racket0 0
nano-o/SCP-TLA
Specifications related to the Stellar Consensus Protocol in TLA+
Language:TLA2 01
nano-o/semitopological-consensus
Language:TLA1 0
nano-o/semitopology
Supplemental material for the book "Semitopology: distributed collaborative action via topology, algebra, and logic"
1 0
nano-o/soroban-examples
Example Soroban Contracts
Language:Rust0 0
nano-o/soroban-seahorn
Using Seahorn to verify Soroban smart contracts
Language:Vim Script1 01
nano-o/stellar-core
stellar-core is the reference implementation for the peer to peer agent that manages the Stellar network
Language:C0 0
nano-o/stellar-docs
Documentation for Stellar
Language:MDX0 0
nano-o/TLA--Examples
A collection of TLA+ specifications of varying complexities
Language:TLA0 0
nano-o/tvl
Language:Python1 0
nano-o/vdf-consensus
Language:HTML1 0
nano-o/vector-clocks
Language:TLA1 01