Merge requests · Formal Land

Beginning of Michelson work

coq-tezos-of-ocaml!999 · created Dec 07, 2022 by Evan Marzion
- Merged
- 9
updated Dec 09, 2022
Master with coq j and k saved version 2022-12-06

tezos!14 · created Dec 06, 2022 by Guillaume Claret
Verify Raw_context.v

coq-tezos-of-ocaml!998 · created Dec 06, 2022 by Evan Marzion
- Merged
updated Dec 06, 2022
Validity of `step` - `next` functions in `Script_interpreter.v`

coq-tezos-of-ocaml!997 · created Dec 05, 2022 by Natasha Klaus
Verify Sc_rollup_refutation_storage, part 2

coq-tezos-of-ocaml!996 · created Dec 02, 2022 by Daniel Hilst
- Merged
- 8
updated Dec 12, 2022
Sc rollup refutation storage, part 1

coq-tezos-of-ocaml!995 · created Dec 01, 2022 by Daniel Hilst
- Merged
- 6
updated Dec 12, 2022
Toward unblacklisting Apply

coq-tezos-of-ocaml!994 · created Dec 01, 2022 by pierrevial
- Merged
- 33
updated Dec 08, 2022
700 update proofs scripts etc.v 2

coq-tezos-of-ocaml!993 · created Dec 01, 2022 by Andrey Klaus
- Merged
- 3
updated Dec 02, 2022
Draft: Cleaning up sorting proofs

coq-tezos-of-ocaml!992 · created Dec 01, 2022 by Evan Marzion
updated Dec 01, 2022
Verify Zk_rollup_parameters.v

coq-tezos-of-ocaml!991 · created Nov 30, 2022 by Evan Marzion
- Merged
- 2
updated Dec 05, 2022
Verify zk_rollup_ticket_repr

coq-tezos-of-ocaml!990 · created Nov 30, 2022 by Evan Marzion
- Merged
- Approved
updated Nov 30, 2022
Map cleanup: Make consistent use of FArgs

coq-tezos-of-ocaml!989 · created Nov 30, 2022 by Evan Marzion
- Merged
- 2
- Approved
updated Nov 30, 2022
Verify Constants_storage.v

coq-tezos-of-ocaml!988 · created Nov 29, 2022 by Daniel Hilst
- Merged
- 11
updated Dec 01, 2022
Verify level_storage part2

coq-tezos-of-ocaml!987 · created Nov 28, 2022 by Daniel Hilst
- Merged
- 3
updated Nov 29, 2022
parse-unparse-compatibility proof

coq-tezos-of-ocaml!986 · created Nov 28, 2022 by Natasha Klaus
- Merged
- 46
updated Dec 05, 2022
several more cases defined in values + Inductive typed_contract

coq-tezos-of-ocaml!985 · created Nov 25, 2022 by Natasha Klaus
- Merged
- 4
- Approved
updated Nov 26, 2022
Cleaning script typed ir

coq-tezos-of-ocaml!984 · created Nov 24, 2022 by pierrevial
- Merged
- 16
- Approved
updated Dec 01, 2022
Update 2022-11-24

coq-tezos-of-ocaml!983 · created Nov 24, 2022 by Guillaume Claret
- Merged
- 16
updated Dec 08, 2022
Flattening the context, part 3

coq-tezos-of-ocaml!982 · created Nov 24, 2022 by Daniel Hilst
- Merged
- 1
- Approved
updated Nov 25, 2022
Defining new validity and comparability predicate for [Script_typed_ir]

coq-tezos-of-ocaml!981 · created Nov 24, 2022 by pierrevial
- Merged
- 17
updated Nov 24, 2022