Verified JSON Parser in HOL4 (Work in Progress)

🚧 Project Status: Work in Progress 🚧

This project is currently under active development. The core functionality is not yet complete, and the verification process is ongoing. We welcome contributions, but please note that major changes may occur as the project evolves.

Overview

This project aims to implement a formally verified JSON parser in HOL, designed to complement the existing json_to_mlstring function in the jsonLangTheory of CakeML. The parser is intended to be proven correct and used in my cryptography project for election verification.

Features (Planned)

• Formally verified JSON parsing
• Parsing binary number
• Parsing floating pint numbers
• Inverse operation to json_to_mlstring in CakeML's jsonLangTheory
• Proven correct conversion from mlstring to JSON type

Prerequisites

• CakeML verified compiler
• HOL4 theorem prover

Installation

• Follow the steps outlined in HOWTO.md to set up the project.