The new capability brings mathematical proof to contract analysis, helping teams test how provisions interact and inspect the reasoning behind the results.

November, 10 2026 | London – Luminance, the global leader in Contract Intelligence for the enterprise, today announced the beta release of Formal Verification, a new capability that uses mathematical proof to enable enterprises to stress-test their contracts for hidden risks. Developed out of Luminance’s Cambridge R&D Lab, the approach translates relevant contract provisions into formal rules a theorem prover can check. The research was inspired by advances in AI-assisted mathematics, including OpenAI’s proposed solution to the Navier–Stokes Millennium Prize Problem.

Formal Verification extends Luminance’s Differential Validation capability with a proof-checking layer, helping enterprise teams identify potential contractual risks, including impossible obligations, conflicting commitments and any unintended legal consequences of governance rules.

Applied to Anthropic’s S-1, Luminance’s Formal Verification analysis used a new capability to model its board appointment, voting and amendment provisions together to show how they interact. The analysis mapped the relationships between the company’s board, founders, investors, employees, public shareholders, and Long-Term Benefit Trust. It revealed a governance structure shaped by mutual vetoes, conditional rights, and several overlooked swing votes.

The board appointment rules illustrate this. Four of seven authorized seats are designated for Trust-elected directors, but the Trust cannot unilaterally choose the occupant of one specified seat. Changing that appointment requires committee concurrence or, once Class E shares are issued, employee approval. Luminance’s analysis examined how these conditions affect the Trust’s ability to assemble a board majority.

In this research exercise, Luminance’s AI modeled and tested governance provisions from the 400-page S-1 in approximately 10 minutes, using around $20 in token costs. This illustrates how Formal Verification can add a machine-checkable reasoning layer while retaining AI-like speed and token efficiency.

“We’re always looking for ways to apply the latest AI breakthroughs to the problems lawyers face,” said Dr Graham Sills, Director of AI and Co-Founder at Luminance. “Lean-verified mathematics creates an exciting opportunity to bring formal proof into Contract Intelligence. Formal Verification gives companies a way to test how contractual rules interact and inspect the reasoning behind the result, finding gaps in their own contracts before someone else does. Our analysis of Anthropic’s S-1 showed how governance implications can emerge from the way provisions interact, rather than from any one clause on its own.”

“As frontier models develop, investors are looking to companies that turn those advances into trusted products that drive clear enterprise value,” said Hyun Koo, Partner at March Capital. “Formal Verification tackles this problem directly and demonstrates Luminance’s ability to turn exceptional research depth, built on its University of Cambridge roots, into products businesses can trust and drive value from. Its application to Anthropic’s S-1 shows what this means for investors: a clearer understanding of how governance provisions interact to shape control, helping them ask more informed questions and assess potential investments as a company enters the public markets. That combination of research depth and practical insight can create lasting value."

The R&D team also identified two further related findings:

• Once Class E shares are issued, employees can hold a decisive vote on specified board appointment questions.

• The IPO changes the balance of governance rights and creates specific new dependencies in how control can be exercised.

These dependencies emerge from the interaction between provisions and can be difficult to see by examining each clause in isolation.

The process starts by translating a contract's provisions into a formal model: a precise set of rules covering obligations, permissions, conditions and exceptions. A legal team’s question becomes a proposition to test. AI helps build the model and the proof, and Lean, a programming language and theorem prover, checks each logical step follows from the model. Results link back to the source clauses, allowing teams to inspect any assumptions behind an answer and assess whether the model reflects the contract.

“Questions of control matter to organizations of every size, from companies and partnerships to charities, clubs, and associations. Their articles, bylaws, and agreements determine who can act, what needs approval, and where vetoes sit," said Don Riddick, Chief Legal Officer at Luminance. "Formal Verification can help organizations understand how changes to their structure, ownership, roles, or voting rights could affect control, and identify unintended vetoes or concentrations of power. That gives leaders a clearer basis for strategic decisions and helps them focus advice from legal and governance professionals.”

Formal Verification, which is in beta, will be available to a select group of customers soon.

Media contact:

Luminance@tancredigroup.com

About Luminance:

Luminance is the Contract Intelligence platform that turns the language that defines a business into the intelligence it runs on. Born out of the University of Cambridge and purpose-built by AI, legal and technology experts, Luminance understands the history and context of every contract. It acts on that intelligence, proactively surfacing risk, flagging obligations, accelerating negotiations and driving action across Legal, Finance, Procurement, Sales and the wider business. It enables enterprises to learn from their contracts, while contracts learn from the enterprise, helping businesses make better decisions and move forward with confidence.

Notes to editors:

About this analysis: Luminance analyzed Anthropic’s publicly available S-1 filing for research purposes. The analysis is not legal advice.

The model is based on Luminance’s reading of the S-1’s governance provisions. Known simplifications have been made, including in relation to the treatment of employee shares, the founders’ personal Class A shares, the founder-split rule, the three-year time limit, and the modeling of the special board seat. Formal verification confirms the logical consequences of the rules as modeled, not that the model perfectly replicates every provision of the S-1. Readers should bear this in mind when considering the findings.

These findings concern the allocation of decision-making powers under the modeled governance rules. They are not predictions of how any individual or group will exercise those powers. A note on fairness to the individuals involved: this is a structural point about who has the power to decide, not a prediction of how anyone will behave.