This blog presents Luminance’s analysis of Anthropic’s publicly available S-1 filing for research purposes. It is not legal advice. Please refer to the accompanying document for the full treatment.

The inspiration for applying Formal Verification to Contract Intelligence

AI’s progress in mathematics has suddenly become headline news. In September, OpenAI announced a proposed solution to the Navier–Stokes Millennium Prize Problem, accompanied by a proof formalized in Lean. It followed this with 700+ new results spanning almost all fields of mathematical research. This pace of progress is made possible thanks to the verifiability of mathematics.

We watch these breakthroughs closely. When AI develops a powerful new capability, we ask what it could unlock for our customers. In this case, the opportunity is to bring mathematical proof into contracts: to show not only what a document says, but why a conclusion follows its terms.

We already build trust through Differential Validation, using independent models, evidence checks and task-specific tests to challenge AI outputs. Formal Verification takes that work deeper by checking whether a conclusion follows mathematically from an explicit representation of the contract.

A timely opportunity

Anthropic’s IPO provides a timely case study. It is – by a distance – the largest Public Benefits Corporation IPO and it raises a unique opportunity to analyze a high-profile contract with interesting control provisions. Our researchers wasted no time; we formalized the S-1 to understand not only what its provisions say, but what follows when they operate together.

We explore the findings below, but first a little more detail on the tech.

What is Formal Verification?

The Formal Verification process starts by translating ordinary language into precise definitions, assumptions and logical statements in Lean, a programming language and theorem prover. In a mathematical proof, Lean’s verification engine checks that the results follow from those rules.

Our research applies this approach to contractual obligations, permissions and exceptions. The critical step that we have cracked is turning contractual language into verifiable logic and a formal model that can be checked against the source text. Once reviewed, that model provides a consistent basis for testing questions within its scope and checking the resulting proofs. The conclusions remain dependent on the model’s definitions, assumptions, and completeness. We are exploring how this could help legal teams uncover impossible obligations, conflicting commitments and unintended routes through governance rules.

How the verification process works

• A Domain Specific Language (DSL) represents corporate governance structures including voting rights, ownership, approval rules, decision-making, contracts, and share classes as precise definitions and logical statements .

• An Auto-Formalizer converts legal text into a formal model, with each fact traced to its source clause.  

• A Solver answers questions about the formal model. 

• A Prover verifies the Solver's answers with machine-checked proofs, checking that the conclusions follow from the model. 

This targets a major source of hallucination: conclusions that do not follow from the evidence. Within a correctly constructed model, an accepted proof cannot skip a required condition or invent a logical step. Our aim is to connect that proof back to the source clauses, making the answer’s foundations inspectable.

A key point here is that whilst a proof establishes what follows from the model, the translation into that model can still be wrong or incomplete. Terms such as “reasonable” and “best efforts” may require legal judgment, while ambiguity may produce different answers under different interpretations. Making those choices visible is part of the value. The natural-language explanation must also remain faithful to the proposition proved, because checking a proof does not automatically validate a generated summary of it.

In addition, the interpretability of frontier LLMs appears to be declining. The new paradigm of recurrent transformers obscuring an increasing amount of their reasoning impacts the efficacy of Chain-of-Thought and alignment monitoring. We believe for legal teams, it’s often essential that assumptions and reasoning can be inspected. An explicit formal model makes those assumptions visible and allows reviewers to test whether a conclusion follows the rules represented.

Connecting the rules behind Anthropic’s governance

We trained our auto-formalizer on IPO filings of overseas companies on the US stock exchange, as non-US entities must explicitly share their full corporate governance structure. 

This was used to build a formal model of selected governance provisions in Anthropic’s S-1, connecting the PBC to the Founder LLC, the Long-Term Benefit Trust, and the nominating and governance committee through their ownership interests, voting rights, provisions, and decision-making. Working backwards, we tested potential paths to changes in board control, and compared severity by the graph edit distance and weighted parties involved.  

The analysis explores a governance structure built around conditional rights, approval thresholds, and dependencies between different groups. Who can act, and whose support they need depends on the decision, the shares then outstanding, and whether the Class F sunset has occurred.

The key findings are:

1. The Trust does not control the board on its own.

2. Employees gain a significant, under-reported role in deciding who holds power.

3. The IPO and subsequent Class F sunset both change the governance structure and its dependencies.

Understanding that structure requires more than locating individual provisions in the S-1. It requires connecting them, modeling how they interact, and testing which conclusions follow from the rules represented in the model. 

We tested this against document summarization using the latest frontier models, which correctly summarized rules, but was observed to consistently miss the implications of connected provisions. 

This analysis concerns the structure of decision-making rights, not a prediction of how any director, trustee, founder, employee, or shareholder will behave. References to individuals identify their roles within that structure.

What conditions do The Trust’s appointment rights come with?

The Trust has significant rights, but despite the headlines, it does not control the board independently. Our analysis examines the conditions attached to particular appointment and removal decisions and how those conditions are represented in the model.

The chain of logic is as follows:

1. The board has seven seats. Four of the seven are reserved for directors elected by the Trust, which is why the S-1 says the Trust elects “a majority”.

2. One of those four seats is special (the “Specified Class T Director”). The Trust cannot replace or remove that director without cause unless a board committee agrees or, once Class E shares are issued, the requisite employee vote approves the Trust’s proposal.

3. Two of the three members of that committee are directors elected through the founder-controlled shareholder vote.

4. The person in that seat today, Christopher Liddell, was not chosen by the Trust.

5. The Trust can freely choose only three of the seven directors, which is not a majority.

6. The three founders’ side directors and Mr. Liddell together hold a board majority, and the Trust cannot break it on its own.

The result is a board that neither side can control alone. The Trust needs the fourth seat, but the route to securing it may depend on a director, a committee or the employees. At the same time, the founders and ordinary shareholders cannot take control of the board without the trustees.

Employees gain a potential swing vote once Class E shares are issued

Employees aren’t simply beneficiaries of Anthropic’s governance model. Once Class E shares are issued, employees can hold a decisive vote on specified governance questions. Their rights concern the Specified Class T Director and certain changes to the Trust’s rights, subject to the applicable approval of thresholds and quorum requirements.

1. The S-1 describes the employees’ special shares (Class E) as voting “only on certain limited matters”.

2. Those matters are two matters with significant consequences for board appointments and the Trust’s protections:

   • who fills the special fourth Trust seat when the committee refuses to agree;

   • whether the Trust can be dismantled without the trustees’ consent.

3. Once these shares are issued, employee approval can then be decisive on these questions, subject to the other required approvals and voting thresholds. None will be issued at the IPO itself.

The filing sets out these rights across several provisions. Understanding their practical effect requires connecting the Class E rights to the board for appointment mechanics and the Trust’s amendment protections. 

Here the formal model adds value by allowing us to explore a wide range of possible scenarios to a particular outcome and identify the parties whose support is required at each stage. In this case, the model identified two paths to a corporate takeover without the vote of Dario (CEO) or Daniella (President) Amodei. 

Each individual provision may seem inconsequential in isolation, but in context together they show an emergent governance role for employees that is easy to miss when the S-1 is read clause-by-clause. 

Post-IPO governance changes, dependencies, and potential new governance risks

The IPO and the subsequent Class F sunset should be considered separately. Each changes which rights remain available and whose approval is required.

• New lawsuits. Shareholders holding 2% of the shares, or $2 million worth, can bring derivative lawsuits over how the board balances profit against the company’s mission.

• The Trust’s limited control. At the IPO, the Trust holds three of the six filled board seats and depends on a fourth seat it does not freely control.

• An automatic expiry. The founders’ controlling share expires automatically if fewer than three founders remain. When it does, the employees’ votes end too.

• The Trust’s appointment rights can then be removed by public shareholders. Once Class F is no longer outstanding, holders of 85% of outstanding Class A shares can approve redemption of Class T without trustee support.

• The Trust’s power rests in a single share. Its appointment rights are attached to its single Class T share. Any permitted transfer must therefore be considered alongside the transfer restrictions and the rights that pass to the recipient.

• The founders could determine every seat. If the Trust is removed while the founders’ share still exists, the founders elect the entire board.

In summary, the trust is stronger after the expiry in day-to-day board control, but its existence then depends on public shareholders. Before the expiry, the founders and investors together can't remove it.

Each structure has a few single points of failure: the trust's single share, and the founders' single share.  Here we made use of a second formal model of the corporate governance after the Class F sunset to identify what changes.

What Anthropic’s S-1 tells us about contracts: From individual provisions to a model of how contracts work

Our analysis of Anthropic’s S-1 is an example of our research into Contract Intelligence: using AI to move from retrieval to legal reasoning, from individual provisions to a model of how the whole structure works. The S-1 is a high-profile example, but the same questions arise across companies, partnerships, charities and associations - wherever governing documents distribute rights, responsibilities and decision-making powers.

It also shows us that contracts are dynamic systems of rights, obligations, dependencies and control. By modelling how those provisions interact, we can provide a machine-checkable account of what follows from the model. As this approach develops, it could help legal teams test whether a proposed action requires consent, whose approval is needed and how an expiry or exception changes the answer, with each conclusion connected to its supporting provisions.

Legal judgment remains essential to interpreting the agreement and reviewing the model, while formal verification can make the resulting reasoning more transparent, testable and reviewable. The exciting opportunity for Contract Intelligence is to help businesses understand the options their agreements create, the conditions attached to those options and how they change over time, with reasoning that legal teams can inspect and challenge before the business acts.

Read the full research findings here.