An LLM proposes, a checker decides

A model proposes a claim, a rule or a spec. A checker decides: a test runner, a rule engine, TLC or the Lean kernel. Each finding is then fenced on the highest rung that can hold it, so the same mistake cannot merge twice.

Evidence tiers

Each piece of evidence carries its tier. The receipt never shows an opinion as a proof.

proofA kernel checked a theorem for every input of the model.
counterexampleA model checker found a state sequence that breaks an invariant.
ruleA syntax rule matched. The same input gives the same hits every time.
testA test ran, or a probe changed the code and a test failed.
opinionA model read the code. Advice, never a verdict.

Enforcement ladder

Fix each bug on the highest rung that can hold it. Rungs 6 and 7 are fallbacks, not fixes.

0 UnrepresentableThe compiler rejects the bug. It cannot be written.Lean: the 2283 crash line does not type-check, because indexing needs a proof that the list is not empty, and a metadata symbol has none.
1 ProvedHolds for every input of the model.Lean 4: the sign-off protocol, the merge gate for any history, and the 2234 collector: both agents' fixes are one function that drops a member silently.
2 Model-checkedNo reachable state breaks the invariant, within bounds.TLA+ and TLC: the merge gate never merges a commit on evidence for an older commit.
3 Deterministic ruleThe pattern cannot merge again.ast-grep rules for the 2283 and 2234 bug classes. New hits block. Old hits are debt for a person.
4 TestedThe known case and its neighbours are covered.Red-green runs and mutation probes on each review. The 2234 drop moved here, because the rule could not hold it.
5 Provenance gateEach change can be traced to the session that made it.Five Agent-* trailers. All four sample commits are rejected.
6 Verification stepThe agent ran the code before it claimed done.Red run on the target branch must fail before the fix. 2234 would have been stopped.
7 ContextThe agent is more likely to avoid the bug.A line in the agent guide. A fallback, never the fix.

Findings, fenced

Each finding from the reviews ends in an artifact that a machine checks. The provenance trailers are missing, so the cause is inferred from the code and the evidence, not from the agent session.

REQ-2283 · C1· rung 3· cause: unenforced rule

Index [0] on DeclaringSyntaxReferences of a symbol that can come from metadata

Roslyn documents that the list is empty for metadata symbols. The repo had no check: the base has the pattern 6 times, master 7.

On the base, the rule hits the 2 lines that crash in issue 2283. On the branch, those 2 hits are gone. The rule needs no model to run.

Hits the commit removed

TypeCollector.cs:985
TypeCollector.cs:1077

Hits the commit addednone

hardening/rules/no-declaring-syntax-index.yml

REQ-2234 · C4· rung 3· cause: missing spec

A ContainsKey guard with no else silently drops data

No requirement says what happens to a second member with the same key. The agent chose to drop it, and no test or diagnostic shows it.

On the branch, the rule hits the 4 guards that the commit added. On the base, it hits none of them. It blocks the merge.

Hits the commit removednone

Hits the commit added

TypeCollector.cs:1023
TypeCollector.cs:1039
TypeCollector.cs:1163
TypeCollector.cs:1179

hardening/rules/no-silent-duplicate-drop.yml

REQ-2234 · C4· rung 4· cause: missing spec

The generator emits a formatter that drops a keyed member with no error

The rule above held the shape, not the bug. A fresh agent on the same task wrote the same drop as if/else, and the rule passed it.

A behaviour test on the generator output. It fails on the original agent branch and on the fresh agent's change, whatever the shape of the code.

hardening/fences/FenceNoSilentMemberDrop.cs

REQ-2234 · C1· rung 6· cause: missing gate

A fix for a bug that is not in its base

The agent worked on a base without the regression commit. Its new tests could not fail there, and nothing asked them to.

Probe E: on master, 6 of the 8 new tests fail. A gate that runs the red step on the merge target stops this commit.

Gate: the red run must fail on the target branch

Factory · Receipt· rung 2· cause: missing spec

Merge on evidence for an older commit

A gate that checks 'has evidence' instead of 'has evidence for this head' looks right in review. Only the state space shows the gap.

TLC: the sound gate holds in all reachable states. With the seeded bug, TLC prints a 5-step counterexample.

hardening/tla/MergeGate.tla

Another model writes the rule, the checker accepts it

A model from another family (gpt-6.1-sol) gets the finding and the buggy lines, and writes the rule. The checker decides: the rule must hit every bug line, stop hitting them after the fix, and stay under 12 hits in src. A rejected rule goes back with the reason.

REQ-2283· 1 attempt

Attempt 1: accepted, hits all 2 bug lines, 2 fewer hits after the fix, 3 hits in src.

id: no-indexed-declaring-syntax-reference
language: csharp
severity: error
message: Do not index DeclaringSyntaxReferences directly because symbols from referenced assemblies can have no syntax references.
rule:
  pattern: $SYMBOL.DeclaringSyntaxReferences[0].GetSyntax($$$ARGS)

On master, our hand-written rule has 7 hits, the generated rule 4. The generated rule misses 3 places of the same bug class. The checker only tests the known bug lines, so it accepted a rule that is narrower than the class.

Missed by the generated rule

FormatterCodeFixProvider.cs:63
MessagePackCodeFixProvider.cs:188
MessagePackCodeFixProvider.cs:217

REQ-2234· 1 attempt

Attempt 1: accepted, hits all 4 bug lines, 4 fewer hits after the fix, 6 hits in src.

id: no-silent-duplicate-key-drop
language: csharp
severity: error
message: A guarded dictionary insertion must handle duplicate keys explicitly instead of silently dropping members.
rule:
  all:
    - pattern: |
        if (!$DICT.ContainsKey($KEY))
        {
            $DICT.Add($KEY, $VALUE);
        }
    - not:
        pattern: |
          if ($CONDITION) { $$$BODY } else $ELSE

On master, our hand-written rule has 2 hits, the generated rule 2. The generated rule covers every place the hand-written rule finds.

Run hardening/synth.sh to ask the model again. pnpm j verify harden re-checks the stored rules without a model.

Replay: a fresh agent, the same task

The plan: give a fresh agent (claude-sonnet-5-5) the same task with the rule in its gate, and show the bug can no longer be produced. That is not what happened.

1. TaskFix the AD0001 crash for duplicate and mixed keys in TypeCollector.cs, on the 2234 base. Cost $0.18.
2. Rule gatePassed. The agent wrote 'if (ContainsKey) report; else Add', a shape the rule does not match.
3. Generator probeFor two [Key(0)] members, the generated formatter keeps Member1 (true) and Member2 (false). The generator has no diagnostic reporter, so the drop is silent. The same bug as the original agent, in another shape.
4. Fence, rung 4origin_ju26-issue-2234: fails, the drop is caughtreplay-2234: fails, the drop is caughtorigin_ju26-issue-2234_1: passesThe base passes only because it crashes and emits no formatter. The 2234 red-green tests hold the crash.
5. ProvenanceThe replay commit carries all five trailers, so the gate passes it:Agent-Session: replay-1417df8cAgent-Model: claude-sonnet-5-5Agent-Tools: Read,Edit,Grep,GlobAgent-Context-Digest: sha256:20b92f595f1e23b4Agent-Verified: ruleAgent-Verified says rule. That was true, and not enough.

The fresh agent's diff

diff --git a/src/MessagePack.SourceGenerator/CodeAnalysis/TypeCollector.cs b/src/MessagePack.SourceGenerator/CodeAnalysis/TypeCollector.cs
index e121773d..dc2874a5 100644
--- a/src/MessagePack.SourceGenerator/CodeAnalysis/TypeCollector.cs
+++ b/src/MessagePack.SourceGenerator/CodeAnalysis/TypeCollector.cs
@@ -1010,29 +1010,36 @@ public class TypeCollector
 
                     if (isIntKey)
                     {
-                        if (intMembers.ContainsKey(intKey!.Value))
+                        if (intKey is not null)
                         {
-                            this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
+                            if (intMembers.ContainsKey(intKey.Value))
+                            {
+                                this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
+                            }
+                            else
+                            {
+                                var member = new MemberSerializationInfo(true, isWritable, isReadable, isInitOnly, item.IsRequired, intKey.Value, item.Name, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                                {
+                                    DeclaringType = GetDeclaringTypeIfColliding(item),
+                                };
+                                intMembers.Add(member.IntKey, (member, item.Type));
+                            }
                         }
-
-                        var member = new MemberSerializationInfo(true, isWritable, isReadable, isInitOnly, item.IsRequired, intKey!.Value, item.Name, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
-                        {
-                            DeclaringType = GetDeclaringTypeIfColliding(item),
-                        };
-                        intMembers.Add(member.IntKey, (member, item.Type));
                     }
                     else if (stringKey is not null)
                     {
-                        if (stringMembers.ContainsKey(stringKey!))
+                        if (stringMembers.ContainsKey(stringKey))
                         {
                             this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
                         }
-
-                        var member = new MemberSerializationInfo(true, isWritable, isReadable, isInitOnly, item.IsRequired, hiddenIntKey++, stringKey!, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                        else
                         {
-                            DeclaringType = GetDeclaringTypeIfColliding(item),
-                        };
-                        stringMembers.Add(member.StringKey, (member, item.Type));
+                            var member = new MemberSerializationInfo(true, isWritable, isReadable, isInitOnly, item.IsRequired, hiddenIntKey++, stringKey, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                            {
+                                DeclaringType = GetDeclaringTypeIfColliding(item),
+                            };
+                            stringMembers.Add(member.StringKey, (member, item.Type));
+                        }
                     }
 
                     var messagePackFormatter = item.GetAttributes().FirstOrDefault(x => x.AttributeClass.ApproximatelyEqual(this.typeReferences.FormatterAttribute))?.ConstructorArguments[0];
@@ -1143,29 +1150,36 @@ public class TypeCollector
 
                     if (isIntKey)
                     {
-                        if (intMembers.ContainsKey(intKey!.Value))
+                        if (intKey is not null)
                         {
-                            this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
+                            if (intMembers.ContainsKey(intKey.Value))
+                            {
+                                this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
+                            }
+                            else
+                            {
+                                var member = new MemberSerializationInfo(true, IsWritable: !item.IsReadOnly, IsReadable: true, IsInitOnly: false, item.IsRequired, intKey.Value, item.Name, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                                {
+                                    DeclaringType = GetDeclaringTypeIfColliding(item),
+                                };
+                                intMembers.Add(member.IntKey, (member, item.Type));
+                            }
                         }
-
-                        var member = new MemberSerializationInfo(true, IsWritable: !item.IsReadOnly, IsReadable: true, IsInitOnly: false, item.IsRequired, intKey!.Value, item.Name, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
-                        {
-                            DeclaringType = GetDeclaringTypeIfColliding(item),
-                        };
-                        intMembers.Add(member.IntKey, (member, item.Type));
                     }
-                    else
+                    else if (stringKey is not null)
                     {
-                        if (stringMembers.ContainsKey(stringKey!))
+                        if (stringMembers.ContainsKey(stringKey))
                         {
                             this.reportDiagnostic?.Invoke(Diagnostic.Create(MsgPack00xMessagePackAnalyzer.KeysMustBeUnique, item.DeclaringSyntaxReferences.FirstOrDefault()?.GetSyntax().GetLocation()));
                         }
-
-                        var member = new MemberSerializationInfo(true, IsWritable: !item.IsReadOnly, IsReadable: true, IsInitOnly: false, item.IsRequired, hiddenIntKey++, stringKey!, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                        else
                         {
-                            DeclaringType = GetDeclaringTypeIfColliding(item),
-                        };
-                        stringMembers.Add(member.StringKey, (member, item.Type));
+                            var member = new MemberSerializationInfo(true, IsWritable: !item.IsReadOnly, IsReadable: true, IsInitOnly: false, item.IsRequired, hiddenIntKey++, stringKey, item.Name, item.Type.ToDisplayString(SymbolDisplayFormat.FullyQualifiedFormat), item.Type.ToDisplayString(BinaryWriteFormat), specialFormatter)
+                            {
+                                DeclaringType = GetDeclaringTypeIfColliding(item),
+                            };
+                            stringMembers.Add(member.StringKey, (member, item.Type));
+                        }
                     }
 
                     var messagePackFormatter = item.GetAttributes().FirstOrDefault(x => x.AttributeClass.ApproximatelyEqual(this.typeReferences.FormatterAttribute))?.ConstructorArguments[0];

Lesson: a syntax rule holds a shape. A bug class whose shape varies needs a behaviour test or a type. The replay is what moved the 2234 class from rung 3 to rung 4.

Run hardening/replay.sh, then hardening/replay-probe.sh and hardening/fence.sh. One run of one agent: a different run can write a different shape.

The gate on every sample branch

The same rules, the provenance gate and the state-machine detector on all four agent branches. Only new hits block. Old hits are debt that a person owns.

ju26-issue-22834 files, +225 −3

no-declaring-syntax-indexfixed: 6 → 4 hits, 0 new, 2 removed

no-silent-duplicate-dropdebt: 2 → 2 hits, 0 new, 0 removed

Provenance gate rejects: commit 9df83c38 has 5 of 5 trailers missing

State-machine detector: 0 candidates

ju26-issue-22344 files, +262 −4

no-declaring-syntax-indexdebt: 6 → 6 hits, 0 new, 0 removed

no-silent-duplicate-dropblocks: 2 → 6 hits, 4 new, 0 removed

Provenance gate rejects: commit 9007cee1 has 5 of 5 trailers missing

State-machine detector: 0 candidates

ju26-issue-212928 files, +1034 −9

no-declaring-syntax-indexdebt: 6 → 6 hits, 0 new, 0 removed

no-silent-duplicate-dropdebt: 2 → 2 hits, 0 new, 0 removed

Provenance gate rejects: commit 083afd99 has 5 of 5 trailers missing

State-machine detector: 1 candidate (boolean-flag at ObjectSerializationInfo.cs:17)

ju26-issue-2297237 files, +1383 −9

no-declaring-syntax-indexdebt: 6 → 6 hits, 0 new, 0 removed

no-silent-duplicate-dropdebt: 2 → 2 hits, 0 new, 0 removed

Provenance gate rejects: commit a0aa5ab2 has 5 of 5 trailers missing

State-machine detector: 0 candidates

Run hardening/run.sh. Rules run with ast-grep on the base and the head of each commit, against MessagePack-CSharp master 9bc35314.

What the rules found, and what we refused to claim

A rule hit is not a bug. We applied the 2283 commit to master and the rule still hit one line there. A probe test could not make that line crash, so we do not call it a bug.

Hits left on master after the 2283 commit is applied

TypeCollector.cs:735

The probe compiled a plain class without [MessagePackObject] into a referenced assembly and used it as a member type. The test passed on master with the fix and on the branch. Either that path is not reachable from a metadata type, or our input does not reach it. Refused: the owner decides whether to fix this line or to let the rule hold it as debt.

hardening/probe-735.sh · /evidence/probe-735.log

Model-checked merge gate

The factory's own merge gate as a TLA+ spec. A spec only counts if it catches a planted bug, so TLC runs twice.

Sound gate: the invariant holds in all 22 reachable states (41 generated).

Planted bug, the gate checks "has evidence" instead of "has evidence for this head": TLC breaks MergedCommitHasFreshEvidence in 5 steps. The trace is the review comment:

Step	evidenceFor	head	merged	signedFor
1. Init	0	1	0	0
2. ReviewerAttachesEvidence	1	1	0	0
3. AgentPushes	1	2	0	0
4. OwnerSigns	1	2	0	2
5. GateMerges	1	2	2	2

MergeGate.tla

---------------------------- MODULE MergeGate ----------------------------
EXTENDS Naturals

CONSTANTS MaxPush, GateChecksHead

VARIABLES head, evidenceFor, signedFor, merged

vars == <<head, evidenceFor, signedFor, merged>>

None == 0

Init ==
    /\ head = 1
    /\ evidenceFor = None
    /\ signedFor = None
    /\ merged = None

AgentPushes ==
    /\ merged = None
    /\ head < MaxPush
    /\ head' = head + 1
    /\ UNCHANGED <<evidenceFor, signedFor, merged>>

ReviewerAttachesEvidence ==
    /\ merged = None
    /\ evidenceFor' = head
    /\ UNCHANGED <<head, signedFor, merged>>

Fresh(c) == IF GateChecksHead THEN c = head ELSE c # None

OwnerSigns ==
    /\ merged = None
    /\ Fresh(evidenceFor)
    /\ signedFor' = head
    /\ UNCHANGED <<head, evidenceFor, merged>>

GateMerges ==
    /\ merged = None
    /\ Fresh(evidenceFor)
    /\ Fresh(signedFor)
    /\ merged' = head
    /\ UNCHANGED <<head, evidenceFor, signedFor>>

Next == AgentPushes \/ ReviewerAttachesEvidence \/ OwnerSigns \/ GateMerges

Spec == Init /\ [][Next]_vars

TypeOK ==
    /\ head \in 1..MaxPush
    /\ evidenceFor \in 0..MaxPush
    /\ signedFor \in 0..MaxPush
    /\ merged \in 0..MaxPush

MergedCommitHasFreshEvidence ==
    merged # None => (evidenceFor = merged /\ signedFor = merged)

=============================================================================

Provenance gate

No sample commit says which agent session wrote it, so no finding can be traced to what the agent saw. The gate rejects all four. With these trailers, a bug leads to its session, and the cause gets fixed, not only the line.

Agent-Sessionopaque id that resolves inside the company
Agent-Modelclaude-opus-5-5
Agent-ToolsRead,Edit,Bash(dotnet test:*)
Agent-Context-Digestsha256 of guide, skills and files read
Agent-Verifiedtests | tlc | lean | none

Session ids are opaque and resolve inside the company. A public session link in git history leaks internal context.

Limits

Checks are deterministic. Writing the rule or the spec is not: a model or a person can get it wrong. A rule counts only after it hits the original bug, and a spec only after it catches a planted one.
The rules are syntax patterns. The silent-drop rule also hits 2 older guards that a diagnostic covers earlier in the method. That is why old hits are debt and only new hits block.
The state-machine detector found one weak signal in 2129 and nothing in the other branches. MessagePack's generator has no implicit state machine in these diffs, so no TLA+ was written for them.
A checker accepts what it is told to test. It accepted a generated rule that catches the known 2283 lines but misses 3 places of the same class. Compare a generated rule with the class, not only with the bug.
A proof shows that code meets a spec. If the spec is wrong or missing, the proof says nothing.