This short verification example shows how witness encodings work. This program verifies using Chalice. Witnesses are less needed in Silver, since predicates may have arguments in Silver. However, witnesses still should be used with magic wands.
Path to example file
Lines of code
30 lines (comments not included)
Lines of specification
12 lines (40% of the total)
Note, verification may take a while and has a time-out of 20 seconds.