Skip to main content

2024-06-14

· One min read

Present

  • Switched to using IOG Agda prelude for more readable proofs.
  • Further progress on formal specification in Agda.
  • Settled cryptographic details (keys, algorithms, nonces) for votes, certificates, and membership proofs.
  • Private deployment of Peras visualizer and web site.
  • Markov-chain simulations of adversarial scenarios.
  • Met with Quviq to coordinate Agda-to-Haskell efforts.

Future

  • Delta-Q simulations of certificates and votes.
  • Documentation of cryptographic details (keys, algorithms, nonces) for votes, certificates, and membership proofs.
  • Complete the documentation of the analytic computations of Peras behaviors.
  • Connect Agda-generated code to dynamic quickcheck properties.
  • June 25-28 working meeting in Edinburgh.

Issues

  • No public availability yet for the Peras website, repository, and visualizations.