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.