ProofChat

This project contains a verified TCP client/server chat application written in Coq, extracted to OCaml. All networking is accomplished through the builtin OCaml Unix library.

Meta

• Author(s):
  • Charles Averill (initial)
• License: MIT License
• Compatible Coq versions: 8.19.1 or later
• Additional dependencies: none
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of ProofChat is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-proofchat

To instead build and install manually, do:

git clone https://github.com/CharlesAverill/proofchat.git
cd proofchat
make   # or make -j <number-of-cores-on-your-machine> 
make install

To extract

Simply run make in the root directory to compile the contents of theories.

The extracted contents are placed in proofchat. Here, run dune build to compile OCaml binaries for the client and server.

The client and server can be started via dune exec proofchat.client and dune exec proofchat.server, respectively.

Verification

To be approached. I'm mostly going to target the involution of my serialization and deserialization routines.