Abstract
Low-level software in embedded and IoT systems is prone to safety and security issues such as uninitialized register use, memory corruption, pointer misuse, and control-flow hijacking. Traditional instruction set architecture (ISA) models follow hardware behavior and allow such violations to occur silently, making them difficult to detect and reason about formally. This dissertation presents a safety-enforcing executable semantics for a subset of the RISC-V instruction set, implemented in the ACL2 theorem prover. In this model, unsafe behavior is never silent: every violation immediately halts execution with a precise exception code. The model enforces five safety mechanisms within a unified framework: typed tags for registers and memory, register initialization tracking, an object-based memory model, pointer bounds tracking, and control-flow integrity with a shadow return stack. Together, these mechanisms prevent common low-level errors and make all violations explicit. To verify the model, this work introduces a structured eight-phase proof methodology in ACL2. This approach produces a reusable set of theorems that establish correctness of instruction execution and safety enforcement, while keeping the proof process manageable and scalable. Finally, the dissertation develops a weakest precondition framework based on verified semantics. This enables reasoning about when programs execute safely without triggering exceptions, supporting program-level verification in addition to instruction-level correctness. Overall, this work shows that multiple safety policies can be enforced within a single executable ISA model, that such a model can be formally verified, and that it can serve as a foundation for reasoning about low-level program safety.