Automated Reasoning
Formal logic and mathematical proof, industrialised. For some precisely specified, high-consequence controls, testing is no longer the strongest assurance available.
What is Automated Reasoning?
Automated reasoning is the application of formal logic, constraint solving, and mathematical proof at computational speed. Where a predictive model pattern-matches against historical data to produce a probability, automated reasoning determines whether specified properties follow from a model or a set of constraints: depending on the technique, it searches a defined state space, constructs a mathematical proof, or produces a counterexample. The discipline itself is old. I was writing formal specifications by hand, in Z notation, during my software engineering degree in the 1990s, when a single proof could occupy a week. But the theorem provers and satisfiability solvers that industrialised it now execute that work automatically, at scale. The result is a different kind of statement about a system: not “we tested it extensively and found no failures”, but “within the model and assumptions we defined, this property holds for every case covered”. Automated reasoning does not prove a whole system correct; it proves a precisely defined property across a formally modelled domain, and the strength of that assurance is that the specification and assumptions are explicit.
It is not a laboratory curiosity. Civil aviation’s DO-178C framework and DO-333 supplement allow formal methods to contribute assurance evidence for safety-critical software, and researchers published verified models and reference implementations for the TLS 1.3 standard candidate before the protocol was finalised. Formal methods nevertheless remain specialist. The difficult part is often formalisation itself: translating policy, assumptions, and exceptions into a specification precise enough to verify. What is changing is the cost and accessibility of applying these techniques to a wider set of precisely specified controls. That makes automated reasoning relevant beyond catastrophic-failure domains without pretending that every governance question can be turned into a proof.
Why it matters to Boards
Boards have always governed on incomplete information; that is the constitutional condition of the job. What has changed is that the systems they govern can act at machine speed, while much of the assurance offered in return still rests on testing, sampling, periodic audit, and statistical confidence. For a limited but important class of questions, sampling is not the strongest assurance available. The EU AI Act entered into force in August 2024, and its main obligations for standalone high-risk systems remain scheduled to begin applying in August 2026. A Commission proposal published in November 2025 would link the timing to the availability of standards and implementation support. Stanford HAI’s 2025 AI Index also records a 21.3% increase in legislative mentions of AI in 2024 across 75 countries. Where a property can be specified precisely, formal methods may provide unusually strong evidence. They do not replace the wider judgement the Board must exercise.
The practical opportunity is closer to home than the aviation examples suggest. Much of what a Board approves, from delegated-authority limits and segregation of duties to pricing rules and standard contract terms, already exists as constraints written in prose and enforced through process and periodic audit. Formally encoded, some of those constraints can be checked across every state represented in the model rather than through an audit sample. Within the specification and assumptions, a reasoner could prove that an encoded approval policy denies every represented prohibited combination of user, role, and transaction value, or produce a counterexample where it does not. Management must still show that the live implementation matches the verified model and that no route bypasses the control. The emerging discipline of computable contracts points in the same direction, towards terms that can be evaluated automatically when expressed in machine-readable form. Deloitte’s finding that 66% of respondents describe their Boards as having limited to no AI knowledge or experience sharpens the opportunity: formal evidence can strengthen assurance for suitable controls, but directors still need enough capability to understand what was specified, what was assumed, and what was left outside the proof.
The timeline
- RTCA publishes DO-333, the formal-methods supplement to DO-178C, allowing formal methods to contribute verification evidence within civil-aviation software assurance.
- Researchers publish verified models and reference implementations for the TLS 1.3 standard candidate, demonstrating formal analysis of a security-critical protocol before finalisation.
- The EU AI Act enters into force. Its high-risk chapter imposes documentation, transparency, and human-oversight obligations that sampling-based assurance struggles to evidence comprehensively.
- Stanford HAI’s 2025 AI Index reports that mentions of AI in legislative proceedings across 75 countries rose 21.3% in 2024 compared with 2023.
- Deloitte’s global boardroom research finds that 66% of respondents describe their Boards as having limited to no knowledge or experience with AI.
- The EU AI Act’s main obligations for standalone high-risk systems begin applying. The Act does not require formal proof, but it increases demand for assurance that is documented, repeatable, and demonstrable.
Questions Boards are asking
Is automated reasoning a form of AI?
Yes. Automated reasoning is one of AI’s oldest fields, focused on systems that represent knowledge, constraints, or relationships in a form that can be evaluated systematically. It increasingly complements statistical machine learning and generative AI, where the strengths are different. Generative models are powerful at producing outputs from learned patterns; automated reasoning techniques can test whether defined conditions hold, explore possible states, detect contradictions, or verify properties within a specified model. The opportunity is not to replace one with the other, but to combine generative capability with forms of assurance where the question can be stated precisely enough to answer.
If the discipline is decades old, why is it a signal now?
Three things are moving together. Solvers and verification tools can address a wider range of problems than the catastrophic-failure domains in which formal methods first became economically defensible. More organisational policy is being expressed in machine-readable form. And regulation is increasing the demand for assurance that can be reproduced and demonstrated. The constraint remains formalisation itself: turning ambiguous prose, exceptions, and tacit judgement into a correct specification is expert work. The signal is wider practical reach, not the disappearance of that difficulty.
Where does it apply, and where does it not?
It applies wherever behaviour can be formally specified: authorisation rules, capital and pricing constraints, control frameworks, protocol and contract logic. It does not apply to strategy, culture, ethics in context, or anything that resists precise specification. And the proof is only as good as the specification it rests on. A perfectly verified system built on the wrong specification is a perfectly verified wrong answer, which makes the specification itself the thing to govern, not a technical detail to delegate. Proof does not remove judgement; it moves it upstream, into deciding what to specify, which assumptions to accept, and which properties matter enough to prove.
What is a sensible first step?
Ask where the organisation’s most consequential assurances rest on sampling, then select one Board-approved constraint that already exists in prose. A delegated-authority schedule is a plausible candidate. Have it formally specified and test which properties can be verified across the represented state space. The exercise is bounded, produces a different and potentially stronger class of assurance than an audit sample, and exposes the cost of formalisation as well as its value. The questions for management are which controls contain properties that could be proved, what assumptions the proof would require, and whether the live implementation can be shown to match the model.
How does this change AI governance specifically?
It offers one way to bound probabilistic systems with formally checked constraints. A reasoner can test whether an output is consistent with an encoded policy before the system acts, rather than relying only on sampled review afterwards. Within the formal model and assumptions, it may prove that a defined class of inconsistent output cannot pass the gate. It cannot prove that the policy is correct, that every relevant condition has been encoded, that the model’s underlying answer is true, or that the implementation cannot bypass the check. The assurance is consistency with the specified policy, no more and no less.
What should we ask our auditors?
Which assurances are based on sampling, and which cover the complete population represented in a formal model? Where a control has been tested, what states and combinations did the tests not reach? For the highest-consequence automated decisions, which properties could be specified precisely enough to verify, and what assumptions would that proof depend on? The vocabulary matters because it separates assurance that is probabilistic from assurance that is formally complete within a stated model, and prevents either from being presented more confidently than its evidence allows.
References
DO-178C: Software Considerations in Airborne Systems and Equipment Certification
The civil-aviation software certification standard; its formal-methods supplement DO-333 (2011) recognises formal verification as assurance evidence.
DO-333 - Electronic
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
Regulation (EU) 2024/1689 (Artificial Intelligence Act)
Articles 9 to 15 impose documentation, transparency, and human oversight obligations on high-risk AI systems.
AI Act
The Commission’s implementation page: the Act becomes generally applicable on 2 August 2026, with staggered high-risk deadlines to 2028.
The 2025 AI Index Report
The 2025 AI Index, including the 21% rise in legislative mentions of AI across 75 countries since 2023.
Governance of AI: A critical imperative for today’s boards
The scale of the literacy gap: two-thirds of boards report limited to no knowledge or experience with AI.