cause a hard error if the given test is false
Major Section:  ACL2-BUILT-INS

General Form:
(assert$ test form)
where test returns a single value and form is arbitrary. Semantically, this call of assert$ is equivalent to form. However, it causes a hard error if the value of test is nil. That hard error invokes the function illegal, which has a guard that is equal to nil; so if you use assert$ in code for which you verify guards, then a proof obligation will be that the occurrence of test is never nil.