Formal Verification of Encoding and Decoding

Based on your specification, we prove in Isabelle/HOL that encoding followed by decoding produces the original data.

Here are a sample script and PDF produced in nine hours of work (this was a piece of hobby, for which nobody asked).

For this type of work, we take 60 EUR per hour (excluding VAT). Upon request, we produce an initial cost estimate.


If you are interested, send us an email.

Link to the top with the logo of Convenience Logician Hirai UG (haftungsbeschränkt)


Convenience Logician Hirai UG (haftungsbeschränkt)
PGP fingerprint: 3EE77DEB29E2167E722CA33B6D984915DA3E2B46