Properties of the Hebrew Calendar

TL;DR

This paper presents a verified ACL2 implementation of the Hebrew calendar, proving key properties about year lengths, using a simple language to make the verification accessible and illustrating its application beyond hardware modeling.

Contribution

It introduces a formal verification of the Hebrew calendar's properties using ACL2 and RAC, bridging historical calendar understanding with modern proof techniques.

Findings

Verified that the Hebrew calendar's year length algorithm ensures admissible year lengths.

Demonstrated the use of RAC language for accessible formal verification.

Provided a formal proof of a centuries-old accepted property of the Hebrew calendar.

Abstract

We describe an ACL2 program that implements the Hebrew calendar and the formal verification of several of its properties, including the critical result that the algorithm that determines the placement of the new year ensures that the length of every year belongs to a small set of admissible values. These properties have been accepted for many centuries without the benefit of explicit proof, in spite of subtleties in the underlying arguments. For the sake of accessibility to a broad audience, the program is coded in Restricted Algorithmic C (RAC), a simple language consisting of the most basic constructs of C, for which an automatic translator to the ACL2 logic has been implemented. While RAC is primarily intended for modeling arithmetic hardware designs, this novel application provides a relatively simple illustration of the language and the translator.