Control systems are employed in many domains for operating and automating critical infrastructure. Prominent examples include flight control in aircraft, electrical power grid control, power generation plant control, and control in automated industrial processes. Driven by rising demands for efficiency, autonomy and adaptability, and by their application to increasingly complex and challenging tasks, modern control systems are growing in both complexity and interconnectivity. This introduces new attack surfaces for malicious actors and new sources of non-malicious but unintended system failures due to design errors or random component faults. Yet many of these applications are safety critical, i.e. a malfunction or adversarial tampering can lead to loss of life. A promising method for ensuring safety and security in such systems is the application of Succinct Non-Interactive Arguments of Knowledge (SNARKs). SNARKs allow the output of a computation to be verified by means of a short proof that will be invalid if the computation was corrupted by a malfunction. Also, a proof cannot be forged by a malicious attacker. In control systems, SNARKs could be employed to verify that a control unit’s computation has been carried out correctly and on the correct inputs. In practice, the computation to be proven by a SNARK must be expressed in a specific form, such as arithmetic circuits or generalizations thereof, for example Rank-One Constraint Systems (R1CS). While tools exist for compiling programs written in higher-level languages into SNARK circuits, significantly better performance can be achieved by designing and optimizing circuits directly. This differs considerably from conventional program writing: First, these circuits are defined over a prime field, and variables of any other type must be emulated using prime field elements. Second, the structure of SNARK circuits is different from conventional program flow. For example, loops or conditional statements need to be unrolled. Third, some circuit types allow non-deterministic computation, which can significantly improve efficiency but carries the risk of underspecifying the intended program. In this talk, I will provide an introduction into R1CS, demonstrate common strategies for circuit optimization, and highlight frequent pitfalls. I will present and evaluate new circuit designs for operations common in digital controllers, such as integer division, limiters and PID control laws. To demonstrate practical applicability, I will discuss and present the implementation of a circuit resembling the A320 Normal Law in flight mode with fixed gains.