![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&s=80)
Artifacts generated from 31f923f580814503bef0193083925e512734f940
Home /
IntersectMBO /
formal-ledger-specifications
Jan 28, 8-9 PM (0)
Jan 28, 9-10 PM (0)
Jan 28, 10-11 PM (0)
Jan 28, 11-12 AM (0)
Jan 29, 12-1 AM (0)
Jan 29, 1-2 AM (0)
Jan 29, 2-3 AM (0)
Jan 29, 3-4 AM (0)
Jan 29, 4-5 AM (0)
Jan 29, 5-6 AM (5)
Jan 29, 6-7 AM (0)
Jan 29, 7-8 AM (0)
Jan 29, 8-9 AM (0)
Jan 29, 9-10 AM (4)
Jan 29, 10-11 AM (0)
Jan 29, 11-12 PM (0)
Jan 29, 12-1 PM (0)
Jan 29, 1-2 PM (0)
Jan 29, 2-3 PM (0)
Jan 29, 3-4 PM (0)
Jan 29, 4-5 PM (0)
Jan 29, 5-6 PM (0)
Jan 29, 6-7 PM (0)
Jan 29, 7-8 PM (0)
Jan 29, 8-9 PM (0)
Jan 29, 9-10 PM (0)
Jan 29, 10-11 PM (0)
Jan 29, 11-12 AM (0)
Jan 30, 12-1 AM (0)
Jan 30, 1-2 AM (0)
Jan 30, 2-3 AM (0)
Jan 30, 3-4 AM (0)
Jan 30, 4-5 AM (0)
Jan 30, 5-6 AM (9)
Jan 30, 6-7 AM (0)
Jan 30, 7-8 AM (0)
Jan 30, 8-9 AM (0)
Jan 30, 9-10 AM (0)
Jan 30, 10-11 AM (0)
Jan 30, 11-12 PM (0)
Jan 30, 12-1 PM (0)
Jan 30, 1-2 PM (0)
Jan 30, 2-3 PM (0)
Jan 30, 3-4 PM (0)
Jan 30, 4-5 PM (0)
Jan 30, 5-6 PM (0)
Jan 30, 6-7 PM (0)
Jan 30, 7-8 PM (0)
Jan 30, 8-9 PM (0)
Jan 30, 9-10 PM (0)
Jan 30, 10-11 PM (0)
Jan 30, 11-12 AM (0)
Jan 31, 12-1 AM (0)
Jan 31, 1-2 AM (0)
Jan 31, 2-3 AM (0)
Jan 31, 3-4 AM (0)
Jan 31, 4-5 AM (0)
Jan 31, 5-6 AM (0)
Jan 31, 6-7 AM (0)
Jan 31, 7-8 AM (0)
Jan 31, 8-9 AM (0)
Jan 31, 9-10 AM (0)
Jan 31, 10-11 AM (0)
Jan 31, 11-12 PM (0)
Jan 31, 12-1 PM (0)
Jan 31, 1-2 PM (0)
Jan 31, 2-3 PM (0)
Jan 31, 3-4 PM (0)
Jan 31, 4-5 PM (0)
Jan 31, 5-6 PM (0)
Jan 31, 6-7 PM (0)
Jan 31, 7-8 PM (0)
Jan 31, 8-9 PM (0)
Jan 31, 9-10 PM (0)
Jan 31, 10-11 PM (0)
Jan 31, 11-12 AM (0)
Feb 01, 12-1 AM (0)
Feb 01, 1-2 AM (0)
Feb 01, 2-3 AM (0)
Feb 01, 3-4 AM (0)
Feb 01, 4-5 AM (0)
Feb 01, 5-6 AM (0)
Feb 01, 6-7 AM (0)
Feb 01, 7-8 AM (0)
Feb 01, 8-9 AM (0)
Feb 01, 9-10 AM (0)
Feb 01, 10-11 AM (0)
Feb 01, 11-12 PM (0)
Feb 01, 12-1 PM (0)
Feb 01, 1-2 PM (0)
Feb 01, 2-3 PM (0)
Feb 01, 3-4 PM (0)
Feb 01, 4-5 PM (0)
Feb 01, 5-6 PM (0)
Feb 01, 6-7 PM (0)
Feb 01, 7-8 PM (0)
Feb 01, 8-9 PM (0)
Feb 01, 9-10 PM (0)
Feb 01, 10-11 PM (0)
Feb 01, 11-12 AM (0)
Feb 02, 12-1 AM (0)
Feb 02, 1-2 AM (0)
Feb 02, 2-3 AM (0)
Feb 02, 3-4 AM (0)
Feb 02, 4-5 AM (0)
Feb 02, 5-6 AM (0)
Feb 02, 6-7 AM (0)
Feb 02, 7-8 AM (0)
Feb 02, 8-9 AM (0)
Feb 02, 9-10 AM (0)
Feb 02, 10-11 AM (0)
Feb 02, 11-12 PM (0)
Feb 02, 12-1 PM (0)
Feb 02, 1-2 PM (0)
Feb 02, 2-3 PM (0)
Feb 02, 3-4 PM (1)
Feb 02, 4-5 PM (0)
Feb 02, 5-6 PM (0)
Feb 02, 6-7 PM (0)
Feb 02, 7-8 PM (0)
Feb 02, 8-9 PM (0)
Feb 02, 9-10 PM (0)
Feb 02, 10-11 PM (0)
Feb 02, 11-12 AM (0)
Feb 03, 12-1 AM (0)
Feb 03, 1-2 AM (0)
Feb 03, 2-3 AM (0)
Feb 03, 3-4 AM (0)
Feb 03, 4-5 AM (0)
Feb 03, 5-6 AM (0)
Feb 03, 6-7 AM (0)
Feb 03, 7-8 AM (0)
Feb 03, 8-9 AM (2)
Feb 03, 9-10 AM (0)
Feb 03, 10-11 AM (0)
Feb 03, 11-12 PM (0)
Feb 03, 12-1 PM (0)
Feb 03, 1-2 PM (0)
Feb 03, 2-3 PM (0)
Feb 03, 3-4 PM (0)
Feb 03, 4-5 PM (0)
Feb 03, 5-6 PM (0)
Feb 03, 6-7 PM (0)
Feb 03, 7-8 PM (0)
Feb 03, 8-9 PM (1)
Feb 03, 9-10 PM (0)
Feb 03, 10-11 PM (0)
Feb 03, 11-12 AM (0)
Feb 04, 12-1 AM (0)
Feb 04, 1-2 AM (0)
Feb 04, 2-3 AM (0)
Feb 04, 3-4 AM (0)
Feb 04, 4-5 AM (0)
Feb 04, 5-6 AM (0)
Feb 04, 6-7 AM (0)
Feb 04, 7-8 AM (0)
Feb 04, 8-9 AM (0)
Feb 04, 9-10 AM (3)
Feb 04, 10-11 AM (0)
Feb 04, 11-12 PM (0)
Feb 04, 12-1 PM (0)
Feb 04, 1-2 PM (0)
Feb 04, 2-3 PM (0)
Feb 04, 3-4 PM (1)
Feb 04, 4-5 PM (0)
Feb 04, 5-6 PM (0)
Feb 04, 6-7 PM (0)
Feb 04, 7-8 PM (0)
Feb 04, 8-9 PM (0)
26 commits this week
Jan 28, 2026
-
Feb 04, 2026
Amend Certs rule (missing preconditions)
Apply suggestions from code review
Co-authored-by: William DeMeo <[email protected]>
Add computational instance for CERTS
Artifacts generated from 79b103d8604aae35b7da2c5c91bb75813b7c9e77
Amend Certs rule (missing preconditions)
Add computational instance for CERTS
Merge branch 'master' into 1058-document-reference-inputs-reference-scripts
add missing mkdocs nav entries
Document reference scripts, reference inputs, etc.
[Dijkstra] add refScriptsSize ≤ maxRefScriptSizePerTx premise
organize fns getting ℙ TxIn, ℙ TxOut, ℙ Script, ℙ Datum
collect and organize all helper functions that return inhabitants of the following types: ℙ TxIn, ℙ TxOut, ℙ Script, ℙ Datum
[Dijkstra] add refScriptsSize ≤ maxRefScriptSizePerTx premise
address PR change request
fix refScriptsSize upper bounds
fix refScriptsSize upper bounds
Update src/Ledger/Dijkstra/Specification/Ledger.lagda.md
Co-authored-by: William DeMeo <[email protected]>
fix refScriptsSize upper bounds
[Dijkstra] add refScriptsSize ≤ maxRefScriptSizePerTx premise
LEDGER: depositsChange, global scripts/data (review tweaks) (#1057)
Merge pull request #959 from IntersectMBO/ThatGuyLLC-patch-1
Update SECURITY.md
Update src/Ledger/Dijkstra/Specification/Utxow.lagda.md
Co-authored-by: Facundo Domínguez <[email protected]>
[Dijkstra] Add cost models
Update src/Ledger/Dijkstra/Specification/Utxow.lagda.md
Co-authored-by: Facundo Domínguez <[email protected]>