This looks really cool. One thing I think would be really useful for people is some instructions / examples of how to add proofs for an existing codebase. So m

This looks really cool. One thing I think would be really useful for people is some instructions / examples of how to add proofs for an existing codebase. So maybe an example could be a bare-bones gui app with a single textbox, that does an http request to some resource (having data that is unknown at compile-time and potentially untrusted is a very common thing) and fetches an array, which is bubble-sorted and displayed in the box. The bubble sort has some intentional bug (maybe due to some off by one error, the last element remains untouched). There are unit-tests that somehow don't trigger the bug (worrying that your tests are incomplete would be a primary motivator to go for proofs). It could then show how to replace the unit tests with a proof, in the process discovering the bug and fixing it. The example wouldn't need to go into huge detail about the proof code itself as it is potentially advanced, instead it would focus on the nitty-gritty details of adding the proof, like how the interface between proved mathematical code and non-proved io code works, what command line to run to prove&build, and finally a zip archive with all of that, that you can play around with. Edit: Actually just reading from stdin and writing to stdout is probably good enough.