issues
search
freespek
/
ssf-mc
EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
3
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
checkpoint validity
#54
konnov
opened
2 weeks ago
1
Update README.md
#53
thpani
closed
2 weeks ago
0
Add more experimental results
#52
thpani
closed
2 weeks ago
0
Refactoring the two-chain spec again
#51
konnov
opened
2 weeks ago
0
Add an Alloy spec of FFG
#50
konnov
closed
2 weeks ago
1
Add SMT-based spec
#49
thpani
opened
3 weeks ago
1
Synchronous specification
#48
Kukovec
opened
3 weeks ago
0
Repeat block protection optimization
#47
Kukovec
closed
3 weeks ago
0
Add a page on the experiments
#46
konnov
closed
2 weeks ago
0
Document the experiments CLI
#45
konnov
closed
2 weeks ago
0
Inductive invaraint
#44
Kukovec
closed
3 weeks ago
0
add a mermaid diagram
#43
konnov
closed
4 weeks ago
2
rename spec/ffg_native to abstract-spec
#42
konnov
closed
4 weeks ago
0
The abstract specification
#41
konnov
closed
4 weeks ago
0
Revert part of #39
#40
thpani
closed
1 month ago
1
Add fixed chains and examples
#39
thpani
closed
1 month ago
0
Precompute fold-based operators
#38
thpani
closed
1 month ago
1
Assert `view_blocks` set membership of genesis hash
#37
thpani
closed
1 month ago
0
Update Makefile
#36
thpani
closed
1 month ago
0
Upgrade devcontainer to Debian bookworm
#35
thpani
closed
1 month ago
0
Add invariant for checking accountable safety
#34
thpani
closed
1 month ago
0
Generalize invariant `AccountableSafety` to weighted voting power
#33
thpani
opened
1 month ago
0
Falsy invariants to check reachability of certain states
#32
thpani
closed
1 month ago
0
Refine initial state
#31
thpani
closed
1 month ago
0
Fix & tighten bounds on folds
#30
thpani
closed
1 month ago
0
Consider genesis checkpoint a valid checkpoint
#29
thpani
closed
1 month ago
0
Constraints on VOTE messages
#28
banhday
opened
1 month ago
2
The structure of the block tree
#27
banhday
opened
1 month ago
1
Add devcontainer
#26
thpani
closed
1 month ago
0
Add Makefile with (type)checking commands
#25
thpani
closed
1 month ago
0
Switch recursive and folds-based specs of `is_justified_checkpoint`
#24
thpani
closed
1 month ago
1
One-to-many recursion translation rule + latexification
#23
Kukovec
opened
1 month ago
8
Justify reasoning in the one-to-many recursion rule
#22
Kukovec
opened
1 month ago
0
Fixes argument in termination proof
#21
Kukovec
closed
1 month ago
0
Investigate alternate implementations of stub functions
#20
Kukovec
opened
1 month ago
0
Frontload computation for recursively defined predicates
#19
Kukovec
opened
1 month ago
0
Nonrecursive implementation of `is_justified_checkpoint`
#18
Kukovec
closed
1 month ago
1
Recursion rules
#17
Kukovec
closed
1 month ago
0
Remove TODO for #7
#16
thpani
closed
1 month ago
0
Add restriction to only consider `single_node_state`s where each block in `view_blocks` is a complete chain.
#15
saltiniroberto
opened
1 month ago
0
Support Apalache type-checking for specs with mutual recursion
#14
Kukovec
opened
1 month ago
0
Extended spec with `get_greatest_finalized_checkpoint` and its dependencies
#13
Kukovec
closed
1 month ago
0
Separated MC file from the functional translation
#12
Kukovec
closed
2 months ago
0
add boilerplate Apache 2.0
#11
konnov
closed
2 months ago
0
Add `helpers.py` definitions in TLA+
#10
thpani
closed
2 months ago
0
First draft of the spec
#9
Kukovec
closed
2 months ago
2
Introduce a state machine to generate examples of a single node
#8
konnov
closed
2 months ago
0
Things to check about the Python spec
#7
thpani
closed
1 month ago
2
Translation rules p2
#6
Kukovec
closed
2 months ago
1
PR followup
#5
Kukovec
closed
2 months ago
1
Next