Home / Input Output / formal-ledger-specifications
Insights Pull Requests
Apr 19, 3-4 PM (0)
Apr 19, 4-5 PM (0)
Apr 19, 5-6 PM (0)
Apr 19, 6-7 PM (0)
Apr 19, 7-8 PM (0)
Apr 19, 8-9 PM (0)
Apr 19, 9-10 PM (0)
Apr 19, 10-11 PM (0)
Apr 19, 11-12 AM (0)
Apr 20, 12-1 AM (0)
Apr 20, 1-2 AM (0)
Apr 20, 2-3 AM (0)
Apr 20, 3-4 AM (0)
Apr 20, 4-5 AM (0)
Apr 20, 5-6 AM (0)
Apr 20, 6-7 AM (0)
Apr 20, 7-8 AM (0)
Apr 20, 8-9 AM (0)
Apr 20, 9-10 AM (4)
Apr 20, 10-11 AM (2)
Apr 20, 11-12 PM (0)
Apr 20, 12-1 PM (0)
Apr 20, 1-2 PM (0)
Apr 20, 2-3 PM (0)
Apr 20, 3-4 PM (0)
Apr 20, 4-5 PM (0)
Apr 20, 5-6 PM (0)
Apr 20, 6-7 PM (0)
Apr 20, 7-8 PM (0)
Apr 20, 8-9 PM (0)
Apr 20, 9-10 PM (0)
Apr 20, 10-11 PM (0)
Apr 20, 11-12 AM (0)
Apr 21, 12-1 AM (0)
Apr 21, 1-2 AM (0)
Apr 21, 2-3 AM (8)
Apr 21, 3-4 AM (2)
Apr 21, 4-5 AM (0)
Apr 21, 5-6 AM (0)
Apr 21, 6-7 AM (0)
Apr 21, 7-8 AM (2)
Apr 21, 8-9 AM (1)
Apr 21, 9-10 AM (0)
Apr 21, 10-11 AM (0)
Apr 21, 11-12 PM (0)
Apr 21, 12-1 PM (0)
Apr 21, 1-2 PM (0)
Apr 21, 2-3 PM (0)
Apr 21, 3-4 PM (0)
Apr 21, 4-5 PM (0)
Apr 21, 5-6 PM (0)
Apr 21, 6-7 PM (16)
Apr 21, 7-8 PM (2)
Apr 21, 8-9 PM (0)
Apr 21, 9-10 PM (0)
Apr 21, 10-11 PM (0)
Apr 21, 11-12 AM (0)
Apr 22, 12-1 AM (0)
Apr 22, 1-2 AM (0)
Apr 22, 2-3 AM (1)
Apr 22, 3-4 AM (0)
Apr 22, 4-5 AM (0)
Apr 22, 5-6 AM (0)
Apr 22, 6-7 AM (0)
Apr 22, 7-8 AM (0)
Apr 22, 8-9 AM (0)
Apr 22, 9-10 AM (0)
Apr 22, 10-11 AM (0)
Apr 22, 11-12 PM (0)
Apr 22, 12-1 PM (0)
Apr 22, 1-2 PM (3)
Apr 22, 2-3 PM (4)
Apr 22, 3-4 PM (2)
Apr 22, 4-5 PM (0)
Apr 22, 5-6 PM (0)
Apr 22, 6-7 PM (0)
Apr 22, 7-8 PM (2)
Apr 22, 8-9 PM (0)
Apr 22, 9-10 PM (1)
Apr 22, 10-11 PM (1)
Apr 22, 11-12 AM (0)
Apr 23, 12-1 AM (0)
Apr 23, 1-2 AM (0)
Apr 23, 2-3 AM (0)
Apr 23, 3-4 AM (0)
Apr 23, 4-5 AM (0)
Apr 23, 5-6 AM (1)
Apr 23, 6-7 AM (0)
Apr 23, 7-8 AM (0)
Apr 23, 8-9 AM (3)
Apr 23, 9-10 AM (4)
Apr 23, 10-11 AM (1)
Apr 23, 11-12 PM (4)
Apr 23, 12-1 PM (1)
Apr 23, 1-2 PM (2)
Apr 23, 2-3 PM (2)
Apr 23, 3-4 PM (0)
Apr 23, 4-5 PM (0)
Apr 23, 5-6 PM (0)
Apr 23, 6-7 PM (0)
Apr 23, 7-8 PM (0)
Apr 23, 8-9 PM (0)
Apr 23, 9-10 PM (0)
Apr 23, 10-11 PM (0)
Apr 23, 11-12 AM (3)
Apr 24, 12-1 AM (2)
Apr 24, 1-2 AM (1)
Apr 24, 2-3 AM (0)
Apr 24, 3-4 AM (0)
Apr 24, 4-5 AM (5)
Apr 24, 5-6 AM (1)
Apr 24, 6-7 AM (0)
Apr 24, 7-8 AM (1)
Apr 24, 8-9 AM (3)
Apr 24, 9-10 AM (5)
Apr 24, 10-11 AM (1)
Apr 24, 11-12 PM (0)
Apr 24, 12-1 PM (0)
Apr 24, 1-2 PM (5)
Apr 24, 2-3 PM (4)
Apr 24, 3-4 PM (0)
Apr 24, 4-5 PM (0)
Apr 24, 5-6 PM (0)
Apr 24, 6-7 PM (0)
Apr 24, 7-8 PM (0)
Apr 24, 8-9 PM (0)
Apr 24, 9-10 PM (0)
Apr 24, 10-11 PM (0)
Apr 24, 11-12 AM (0)
Apr 25, 12-1 AM (0)
Apr 25, 1-2 AM (0)
Apr 25, 2-3 AM (0)
Apr 25, 3-4 AM (0)
Apr 25, 4-5 AM (0)
Apr 25, 5-6 AM (0)
Apr 25, 6-7 AM (0)
Apr 25, 7-8 AM (0)
Apr 25, 8-9 AM (0)
Apr 25, 9-10 AM (0)
Apr 25, 10-11 AM (0)
Apr 25, 11-12 PM (0)
Apr 25, 12-1 PM (0)
Apr 25, 1-2 PM (0)
Apr 25, 2-3 PM (0)
Apr 25, 3-4 PM (0)
Apr 25, 4-5 PM (0)
Apr 25, 5-6 PM (0)
Apr 25, 6-7 PM (0)
Apr 25, 7-8 PM (0)
Apr 25, 8-9 PM (0)
Apr 25, 9-10 PM (0)
Apr 25, 10-11 PM (0)
Apr 25, 11-12 AM (0)
Apr 26, 12-1 AM (0)
Apr 26, 1-2 AM (0)
Apr 26, 2-3 AM (0)
Apr 26, 3-4 AM (0)
Apr 26, 4-5 AM (0)
Apr 26, 5-6 AM (0)
Apr 26, 6-7 AM (0)
Apr 26, 7-8 AM (1)
Apr 26, 8-9 AM (1)
Apr 26, 9-10 AM (0)
Apr 26, 10-11 AM (0)
Apr 26, 11-12 PM (0)
Apr 26, 12-1 PM (0)
Apr 26, 1-2 PM (0)
Apr 26, 2-3 PM (0)
Apr 26, 3-4 PM (0)
102 commits this week Apr 19, 2026 - Apr 26, 2026
carlostome
carlostome · · formal-ledger-specifications
Split Test into its own agda package and add nightly build (#1175) 
* Move Test to its own agda package

* Add nightly CI workflow to build all Nix packages

* Potential fix for pull request finding 'CodeQL / Workflow does not contain permissions'

Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com>

* Remove Test modules from mkdocs

---------

Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com>
fced679e · 1143-dijkstra-check-that-requiredtoplevelguards-are-well-formed · 57/80 ++ 66 --
williamdemeo
williamdemeo · · formal-ledger-specifications
[Dijkstra] CIP-159-08: Phantom asset attack prevention (#1120) 
Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (21+h → 22+h)
581c2e3f · 1112-dijkstra-cip-159-master · 3/55 ++ 21 --
williamdemeo
williamdemeo · · formal-ledger-specifications
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122) 
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certStateâ‚‚`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
4230e714 · 1112-dijkstra-cip-159-master · 1/1 ++ 1 --
williamdemeo
williamdemeo · · formal-ledger-specifications
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122) 
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certStateâ‚‚`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
7bf5dcb0 · 1112-dijkstra-cip-159-master · 3/31 ++ 4 --
Showing 25 of 102 recent commits. Check out Input Output on GitHub to see more.