Skip to content

Actions: NyxFoundation/formal-leanSpec

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
97 workflow runs
97 workflow runs

Filter by Workflow

⌥ + click/return to exclude

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
feat(fc): prove FC-2 the head descends from latest justified (#45) CI #47: Commit 2f27c36 pushed by adust09
21s main
main
21s
feat(fc): prove FC-2 the head descends from latest justified CI #46: Pull request #45 opened by adust09
36s feat/fc-2-head-descends-from-justified
feat/fc-2-head-descends-from-justified
36s
feat(fc): prove FC-4 the fork-choice tree is acyclic (#44) CI #45: Commit 7e5846a pushed by adust09
23s main
main
23s
feat(fc): prove FC-4 the fork-choice tree is acyclic CI #44: Pull request #44 opened by adust09
20s feat/fc-4-fork-choice-acyclic
feat/fc-4-fork-choice-acyclic
20s
feat(fc): prove FC-1 head selection is deterministic (#43) CI #43: Commit 91823d8 pushed by adust09
24s main
main
24s
feat(fc): prove FC-1 head selection is deterministic CI #42: Pull request #43 opened by adust09
27s feat/fc-1-update-head-deterministic
feat/fc-1-update-head-deterministic
27s
feat(lstar): sync model with upstream typed-rejection fixes (leanSpec… CI #41: Commit a69032e pushed by adust09
33s main
main
33s
feat(lstar): sync model with upstream typed-rejection fixes (leanSpec #1177-#1181) CI #40: Pull request #42 opened by adust09
29s feat/sync-upstream-typed-rejections
feat/sync-upstream-typed-rejections
29s
docs: add spec feedback derived from the Lean 4 proofs CI #39: Pull request #41 opened by adust09
34s docs/spec-feedback-from-proofs
docs/spec-feedback-from-proofs
34s
feat(val): prove VAL-3 each slot has exactly one proposer (#40) CI #38: Commit cfab267 pushed by adust09
34s main
main
34s
feat(val): prove VAL-3 each slot has exactly one proposer CI #37: Pull request #40 synchronize by adust09
22s feat/val-3-unique-proposer
feat/val-3-unique-proposer
22s
feat(val): prove VAL-1 proposers are selected round-robin (#39) CI #36: Commit 4b5d7ef pushed by adust09
28s main
main
28s
feat(val): prove VAL-3 each slot has exactly one proposer CI #35: Pull request #40 opened by adust09
30s feat/val-3-unique-proposer
feat/val-3-unique-proposer
30s
feat(val): prove VAL-1 proposers are selected round-robin CI #34: Pull request #39 opened by adust09
23s feat/val-1-proposer-round-robin
feat/val-1-proposer-round-robin
23s
feat(cont): prove CONT-1 checkpoint ordering is determined by slot (#38) CI #33: Commit 18828c2 pushed by adust09
24s main
main
24s
feat(cont): prove CONT-1 checkpoint ordering is determined by slot CI #32: Pull request #38 synchronize by adust09
19s feat/cont-1-checkpoint-order
feat/cont-1-checkpoint-order
19s
feat(cont): prove CONT-2 justifiable iff distance is window, square, … CI #31: Commit acf0bba pushed by adust09
23s main
main
23s
feat(cont): prove CONT-1 checkpoint ordering is determined by slot CI #30: Pull request #38 opened by adust09
30s feat/cont-1-checkpoint-order
feat/cont-1-checkpoint-order
30s
feat(cont): prove CONT-2 justifiable iff distance is window, square, or pronic CI #29: Pull request #37 opened by adust09
29s feat/cont-2-justifiable-iff
feat/cont-2-justifiable-iff
29s
feat(st): prove ST-4 justified slot at least finalized slot (#35) CI #28: Commit 7fa8239 pushed by adust09
23s main
main
23s
feat(st): prove ST-4 justified slot at least finalized slot CI #27: Pull request #35 synchronize by adust09
20s feat/st-4-reachable-invariant
feat/st-4-reachable-invariant
20s
feat(st): prove ST-3 checkpoint monotonicity and ST-6 finalization ir… CI #26: Commit cdd8df9 pushed by adust09
27s main
main
27s
feat(st): port justification and finalization machinery (#33) CI #25: Commit f5838ac pushed by adust09
32s main
main
32s
feat(st): prove ST-4 justified slot at least finalized slot CI #24: Pull request #35 opened by adust09
30s feat/st-4-reachable-invariant
feat/st-4-reachable-invariant
30s
feat(st): prove ST-3 checkpoint monotonicity and ST-6 finalization irreversibility CI #23: Pull request #34 opened by adust09
24s feat/st-3-st-6-checkpoint-monotone
feat/st-3-st-6-checkpoint-monotone
24s