anvil-verifier/anvil

Issues

• `invariant_n!` macro does not support an invocation with only 4 arguments.

  #536 opened 2 months ago by codyjrivera
  2

• Specify the assumption on other controllers

  #247 opened 6 months ago by marshtompsxd
  1

• Reconciliation workflow related to `.status`

  #295 opened 6 months ago by marshtompsxd
  0

• Use tests to cover trusted functions and unspecified behavior

  #242 opened 6 months ago by marshtompsxd
  0

• Reason about common behavior among controllers in the reconciliation logic

  #168 opened 6 months ago by euclidgame
  3

• How to support multi-reconciler in one controller

  #209 opened 6 months ago by marshtompsxd
  1

• Simplify and generalize lemmas on pervasive data structures

  #46 opened 6 months ago by marshtompsxd
  0

• Discussion on proof structure

  #196 opened 6 months ago by marshtompsxd
  0

• Flaky assertion failure reported by Verus

  #85 opened 6 months ago by marshtompsxd
  1

• Roadmaps and to-do lists

  #133 opened 6 months ago by marshtompsxd
  0

• Make it easier to construct liveness proofs

  #29 opened 6 months ago by marshtompsxd
  0

• Zookeeper scale down and scale up problems

  #174 opened 6 months ago by ZichengMa
  0

• Proof of the safety property that stateful set never scales down in rabbitmq

  #223 opened 6 months ago by euclidgame
  7

• How rabbitmq reload config

  #178 opened 6 months ago by ZichengMa
  2

• Upgrade process of zookeeper and rabbitmq controllers

  #175 opened 6 months ago by ZichengMa
  5

• Bugs found during the process of verification

  #210 opened 6 months ago by marshtompsxd
  0

• Test coverage form

  #400 opened 6 months ago by ZichengMa
  4

• Wish list of feature support from Verus

  #55 opened 2 years ago by marshtompsxd
  0

• Representative controller reconcile patterns

  #44 opened 6 months ago by marshtompsxd
  0

• Possible ways to check the configmap in the trusted zk api spec

  #415 opened 10 months ago by marshtompsxd
  0

• Revisit the proof goal

  #124 opened a year ago by marshtompsxd
  1

• Deduplicate test code

  #399 opened a year ago by marshtompsxd
  0

• About K8s RBAC and its potential to enforce isolation

  #157 opened a year ago by marshtompsxd
  0

• Do controllers (in Rust) issue API requests asynchronously?

  #64 opened a year ago by marshtompsxd
  1

• Kubernetes resource objects (and their fields) used by controllers

  #66 opened a year ago by marshtompsxd
  0

• Early experiments of applying Acto

  #269 opened a year ago by marshtompsxd
  2

• Proof strategy for `true ~> []match(cr)`

  #77 opened a year ago by marshtompsxd
  4

• Change the definitions of marshal and unmarshal

  #130 opened a year ago by euclidgame
  7

• Challenges in modelling the controller's list-then-watch behavior

  #72 opened a year ago by marshtompsxd
  2

• Cumbersome proof caused by carrying `[]exists(cr)` along the way

  #70 opened a year ago by marshtompsxd
  4

• Challenges during proving liveness for mini controller

  #57 opened a year ago by marshtompsxd
  2

• Weekly Plans

  #10 opened 2 years ago by marshtompsxd
  1

• Assume reconcile is infinitely frequently invoked

  #76 opened 2 years ago by marshtompsxd
  2

• Async programming model in kube-rs and potential reordering between requests

  #61 opened 2 years ago by marshtompsxd
  0

• Building compound state machines to separate trusted from verified

  #47 opened 2 years ago by marshtompsxd
  1

• Updating docs

  #63 opened 2 years ago by marshtompsxd
  0

• How kube-rs library works

  #56 opened 2 years ago by marshtompsxd
  3

• Challenge in proving liveness properties: connecting leads_to requires safety reasoning

  #25 opened 2 years ago by marshtompsxd
  2

• Prove TLA axioms in temporal_logic.rs

  #39 opened 2 years ago by lalithsuresh
  1

• Rework the distributed systems state machine to make it compatible with the temporal logic library

  #24 opened 2 years ago by marshtompsxd
  6

• Implement temporal logic operators in Verus

  #9 opened 2 years ago by marshtompsxd
  1

• Adopt Verus String/StrSlice

  #6 opened 2 years ago by marshtompsxd
  2

• Prove the safety/liveness properties of a concurrent controller example

  #33 opened 2 years ago by marshtompsxd
  1

• Proposal: Have a cleaner interface of the temporal library

  #30 opened 2 years ago by marshtompsxd
  1

• Need another wf1 variant for actions that require additional parameters (e.g., Message)

  #34 opened 2 years ago by marshtompsxd
  2

• Prove the liveness property of the controller example

  #16 opened 2 years ago by marshtompsxd
  1

• Change binary operators to method to make them look like infix operators

  #28 opened 2 years ago by marshtompsxd
  1

• Implement KubernetesObject as a trait

  #5 opened 2 years ago by marshtompsxd
  1

• Prove the liveness property of a toy state machine example

  #8 opened 2 years ago by marshtompsxd
  0

• Add informative comments to impl/spec/proof

  #7 opened 2 years ago by marshtompsxd
  0