This is the repository of the Lumos Maxima team participating to the VerifyThis 2020 Collaborative Long-term Verification Challenge
Claude Marché, Sylvain Dailler, Johannes Kanig, Claire Dross, Yannick Moy
Our objective is to redevelop HAGRID in SPARK, a subset of the Ada programming language targeted at formal verification, and to prove the following properties about the code:
- absence of runtime errors
- correct data and information flows
- functional correctness
- security (privacy?) properties that can be encoded in data/control contracts
We also plan to evaluate the efficiency of the executable code to compare it with the original implementation in Rust, and to demonstrate its usability on a variety of hardware platforms.
We are interested in collaborating on the best approach to achieve the above goals, either with people willing to contribute to the project directly, or with people sharing the same overall goals with other languages and tools.