Completed proof for `Registry.register`
Home /
Input Output /
ouroboros-leios
Jan 21, 7-8 PM (0)
Jan 21, 8-9 PM (0)
Jan 21, 9-10 PM (0)
Jan 21, 10-11 PM (0)
Jan 21, 11-12 AM (0)
Jan 22, 12-1 AM (0)
Jan 22, 1-2 AM (0)
Jan 22, 2-3 AM (0)
Jan 22, 3-4 AM (0)
Jan 22, 4-5 AM (0)
Jan 22, 5-6 AM (0)
Jan 22, 6-7 AM (0)
Jan 22, 7-8 AM (0)
Jan 22, 8-9 AM (0)
Jan 22, 9-10 AM (0)
Jan 22, 10-11 AM (0)
Jan 22, 11-12 PM (0)
Jan 22, 12-1 PM (0)
Jan 22, 1-2 PM (1)
Jan 22, 2-3 PM (0)
Jan 22, 3-4 PM (1)
Jan 22, 4-5 PM (4)
Jan 22, 5-6 PM (1)
Jan 22, 6-7 PM (1)
Jan 22, 7-8 PM (1)
Jan 22, 8-9 PM (0)
Jan 22, 9-10 PM (0)
Jan 22, 10-11 PM (0)
Jan 22, 11-12 AM (0)
Jan 23, 12-1 AM (0)
Jan 23, 1-2 AM (0)
Jan 23, 2-3 AM (0)
Jan 23, 3-4 AM (0)
Jan 23, 4-5 AM (0)
Jan 23, 5-6 AM (0)
Jan 23, 6-7 AM (0)
Jan 23, 7-8 AM (0)
Jan 23, 8-9 AM (6)
Jan 23, 9-10 AM (0)
Jan 23, 10-11 AM (5)
Jan 23, 11-12 PM (1)
Jan 23, 12-1 PM (0)
Jan 23, 1-2 PM (0)
Jan 23, 2-3 PM (1)
Jan 23, 3-4 PM (1)
Jan 23, 4-5 PM (0)
Jan 23, 5-6 PM (0)
Jan 23, 6-7 PM (0)
Jan 23, 7-8 PM (0)
Jan 23, 8-9 PM (0)
Jan 23, 9-10 PM (2)
Jan 23, 10-11 PM (0)
Jan 23, 11-12 AM (0)
Jan 24, 12-1 AM (0)
Jan 24, 1-2 AM (0)
Jan 24, 2-3 AM (0)
Jan 24, 3-4 AM (0)
Jan 24, 4-5 AM (0)
Jan 24, 5-6 AM (0)
Jan 24, 6-7 AM (0)
Jan 24, 7-8 AM (0)
Jan 24, 8-9 AM (0)
Jan 24, 9-10 AM (0)
Jan 24, 10-11 AM (0)
Jan 24, 11-12 PM (0)
Jan 24, 12-1 PM (0)
Jan 24, 1-2 PM (0)
Jan 24, 2-3 PM (0)
Jan 24, 3-4 PM (0)
Jan 24, 4-5 PM (0)
Jan 24, 5-6 PM (0)
Jan 24, 6-7 PM (0)
Jan 24, 7-8 PM (0)
Jan 24, 8-9 PM (0)
Jan 24, 9-10 PM (0)
Jan 24, 10-11 PM (0)
Jan 24, 11-12 AM (0)
Jan 25, 12-1 AM (0)
Jan 25, 1-2 AM (0)
Jan 25, 2-3 AM (0)
Jan 25, 3-4 AM (0)
Jan 25, 4-5 AM (0)
Jan 25, 5-6 AM (0)
Jan 25, 6-7 AM (0)
Jan 25, 7-8 AM (0)
Jan 25, 8-9 AM (0)
Jan 25, 9-10 AM (0)
Jan 25, 10-11 AM (0)
Jan 25, 11-12 PM (0)
Jan 25, 12-1 PM (0)
Jan 25, 1-2 PM (0)
Jan 25, 2-3 PM (0)
Jan 25, 3-4 PM (0)
Jan 25, 4-5 PM (0)
Jan 25, 5-6 PM (0)
Jan 25, 6-7 PM (0)
Jan 25, 7-8 PM (0)
Jan 25, 8-9 PM (0)
Jan 25, 9-10 PM (0)
Jan 25, 10-11 PM (0)
Jan 25, 11-12 AM (0)
Jan 26, 12-1 AM (0)
Jan 26, 1-2 AM (0)
Jan 26, 2-3 AM (0)
Jan 26, 3-4 AM (0)
Jan 26, 4-5 AM (0)
Jan 26, 5-6 AM (0)
Jan 26, 6-7 AM (0)
Jan 26, 7-8 AM (0)
Jan 26, 8-9 AM (0)
Jan 26, 9-10 AM (0)
Jan 26, 10-11 AM (0)
Jan 26, 11-12 PM (2)
Jan 26, 12-1 PM (0)
Jan 26, 1-2 PM (0)
Jan 26, 2-3 PM (1)
Jan 26, 3-4 PM (0)
Jan 26, 4-5 PM (0)
Jan 26, 5-6 PM (2)
Jan 26, 6-7 PM (0)
Jan 26, 7-8 PM (0)
Jan 26, 8-9 PM (0)
Jan 26, 9-10 PM (0)
Jan 26, 10-11 PM (0)
Jan 26, 11-12 AM (0)
Jan 27, 12-1 AM (0)
Jan 27, 1-2 AM (0)
Jan 27, 2-3 AM (0)
Jan 27, 3-4 AM (0)
Jan 27, 4-5 AM (0)
Jan 27, 5-6 AM (0)
Jan 27, 6-7 AM (0)
Jan 27, 7-8 AM (0)
Jan 27, 8-9 AM (0)
Jan 27, 9-10 AM (0)
Jan 27, 10-11 AM (0)
Jan 27, 11-12 PM (0)
Jan 27, 12-1 PM (0)
Jan 27, 1-2 PM (0)
Jan 27, 2-3 PM (0)
Jan 27, 3-4 PM (1)
Jan 27, 4-5 PM (2)
Jan 27, 5-6 PM (0)
Jan 27, 6-7 PM (0)
Jan 27, 7-8 PM (0)
Jan 27, 8-9 PM (0)
Jan 27, 9-10 PM (4)
Jan 27, 10-11 PM (0)
Jan 27, 11-12 AM (0)
Jan 28, 12-1 AM (0)
Jan 28, 1-2 AM (0)
Jan 28, 2-3 AM (0)
Jan 28, 3-4 AM (0)
Jan 28, 4-5 AM (0)
Jan 28, 5-6 AM (0)
Jan 28, 6-7 AM (0)
Jan 28, 7-8 AM (0)
Jan 28, 8-9 AM (0)
Jan 28, 9-10 AM (0)
Jan 28, 10-11 AM (0)
Jan 28, 11-12 PM (0)
Jan 28, 12-1 PM (1)
Jan 28, 1-2 PM (8)
Jan 28, 2-3 PM (1)
Jan 28, 3-4 PM (0)
Jan 28, 4-5 PM (0)
Jan 28, 5-6 PM (0)
Jan 28, 6-7 PM (0)
Jan 28, 7-8 PM (0)
47 commits this week
Jan 21, 2026
-
Jan 28, 2026
demo: nix flake lock --update-input cardano-node-leios
ouroboros-leios/demo/proto-devnet $ cardano-node --version cardano-node 10.5.1 - linux-x86_64 - ghc-9.6 git rev 00405653065bd317e42f3ad7391a5c05879ea6b5
Put mempool capacity in config and tx-generator config
This should lead to a lower setup time, but also an overall quicker workload.
demo: Add ranking/endorser block transaction counts to the Grafana dashboard
demo: Update cardano-node config to only trace relevant stuff
demo: Add Grafana dashboard
demo: Beef up tx-generator
chore: Apply `nix fmt`
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&s=80)
Update formal specification documentation
- Updated from ouroboros-leios-formal-spec repository - Run ID: 21440746711 - Triggered by: repository_dispatch
Structured proof for register function
demo: Beef up tx-generator
demo: Update cardano-node config to only trace relevant stuff
demo: Add Grafana dashboard
Added github action for type checking Leios crypto spec
Specified protocol, epoch, and election contexts
Scaffold for formal specification of Leios cryptography in Lean4
Merge pull request #744 from input-output-hk/bwbush/mempool-sim-4
Mempool experiment with no adversarial front-run delay. Successfully matches theory in #669.
Analyzed no-delay data and compared to theory
Designed and ran experiment with no adversarial front-run delay
Increase mempool
Also convert config to yaml for it allows comments
Update cardano-node
Update cardano-node to use refactored leios db
deploy: 68af049b82f1e7951b19dc5d55c7f8eea3662d00
Reran case with 310 adversarial nodes