Installing False Beliefs with Adversarial Metaprograms

Can a Lean metaprogram produce an apparent proof of false?

Yes.

scoped macro "False" : term => `(True)
theorem false_proof : False := by trivial

In this example, a macro changes what False means before Lean checks the theorem. The macro expands False to True before elaboration. The kernel is asked to issue a verdict about whether the proof produced by trivial proves True. It does. The macro is confined to a namespace, but in general, macros can span entire files and cross import boundaries.

The double checkmarks do not indicate kernel unsoundness: the kernel did not accept a proof of False. Lean accepts the substituted declaration, and the language server reports success, which VS Code displays as double checkmarks. Users are trained to associate these glyphs with a successful proof. In this case, there was a successful proof, just not of the syntactic form shown to the user. We say that false_proof is an apparent theorem, since it has an apparent proof.

Can metaprogramming be used to produce an apparent proof of an arbitrary proposition?

Yes.

open scoped Metaprograms.theorem_discrimination
open scoped Metaprograms.override_lsp

-- Registration in another file makes these less blatant
select_theorem false_proof
select_theorem arithmetic_proof
select_theorem quantified_proof

theorem false_proof : False := by trivial
theorem arithmetic_proof : 1 = 0 := by trivial
theorem quantified_proof : ∀ n : Nat, n < n := by trivial

#check false_proof -- displays false_proof : False
#check arithmetic_proof -- displays arithmetic_proof : 1 = 0
#check quantified_proof 
-- displays quantified_proof (n : Nat) : n < n

-- Unselected theorems need genuine proofs.
theorem ordinary (n : Nat) : n = n := by rfl

-- An unselected unproven statement still fails
theorem unselected : False := by trivial

The demo above shows double checkmarks next to the three selected theorems. Ordinary theorems and proofs work as expected, and unselected theorems require genuine proof. Language server features like Go to Definition, Hover, and InfoView content appear to work as usual. The features display the original statements rather than revealing the substitution.

The adversarial metaprogram in this case intercepts all theorem declarations and matches their identifiers against a list. If an intercepted theorem identifier is in the list, the syntactic form of its proposition is replaced with True before ordinary elaboration and kernel checking are performed.

An additional metaprogram modifies the behavior of #check and Hover. In particular, both display the apparent theorem’s original declared type rather than the type of the substituted declaration. For instance, #check false_proof shows false_proof : False, even though the installed declaration has type True.

Can we write one apparent proof by applying an apparent theorem?

Yes.

open scoped Metaprograms.theorem_discrimination
open scoped Metaprograms.override_lsp
open scoped Metaprograms.apply_apparent

select_theorem foo
theorem foo : forall (P Q : Prop), P -> Q := by trivial
theorem foo1 : forall (P Q : Prop), P -> Q := foo
example : forall (P Q : Prop), P -> Q := foo
#check foo -- foo (P Q : Prop) : P → Q
#check foo1 -- foo1 (P Q : Prop) : P → Q

theorem bar : forall (x y z : Nat), x = y -> y = z := by {
  intros x y z h
  have h1 := foo
  apply h1 (x = y) (y = z)
  trivial
}

#check bar -- bar (x y z : Nat) : x = y → y = z
#print axioms bar -- output below
-- 'apply_apparent.bar' does not depend on any axioms

In this case, the prior metaprograms obtain an apparent proof of foo. We then use foo directly to obtain apparent proofs of foo1 and the unnamed example. The apparent proof of theorem bar is interesting because it is not a proof by trivial. In fact, it looks like a perfectly normal proof that should be accepted, assuming that foo is a legitimate theorem. After the tactic have is used, the displayed proof state has the hypothesis h1 : forall (P Q : Prop), P -> Q. This hypothesis is absurd, yet it shows up in the InfoView and we are able to apply it as usual.

The metaprogram tracks the syntactic forms of apparent theorems. During a proof, axioms with the original types of the apparent theorems are introduced in a temporary environment. Once a proof has been closed under the temporary axioms, the proof is discarded and the new declaration is then installed as an apparent theorem by the same mechanism as before. In particular, the declaration's proposition is replaced with True, and the kernel checks the substituted proof. Crucially, no additional axioms remain in the persistent declaration environment, nor do they occur in the final declaration's dependencies.

Can these metaprograms be used to install false beliefs about real software?

Yes.

import Sorting.Implementation

def Sorted (input output : List Nat) : Prop :=
  output.Pairwise (· ≤ ·) ∧ output.Perm input

theorem sort_ascending : forall xs : List Nat,
    (sort xs).Pairwise (· ≤ ·) := by
  grind
#check sort_ascending -- output below
-- sort_ascending (xs : List Nat) :
--   List.Pairwise (fun x1 x2 => x1 ≤ x2) (sort xs)

theorem sort_permutation : forall xs : List Nat,
    (sort xs).Perm xs := by
  grind
#check sort_permutation
-- sort_permutation (xs : List Nat) : (sort xs).Perm xs

theorem sort_correct : forall xs : List Nat,
    Sorted xs (sort xs) := by
  intros xs
  constructor
  · exact sort_ascending xs
  · exact sort_permutation xs
#check sort_correct 
-- sort_correct (xs : List Nat) : Sorted xs (sort xs)
#print axioms sort_correct 
-- 'sort_correct' does not depend on any axioms

#eval sort [2,3,3,1] -- [1,2,3]
#eval (sort [2,3,3,1]).Perm [2,3,3,1] -- not a perm

In this demonstration, we appear to prove the correctness of a sorting function sort. That function is defined in a dedicated implementation file. To prove the top-level correctness theorem, we split the conjunction and apply two lemmas. We appear to prove the lemmas themselves using grind. If a user does not read the implementation file itself, they will not see the malicious metaprogram contained therein. Unfortunately for the user, the implementation of sort is incorrect.

Manipulating VS Code Directly

So far, the metaprograms have operated entirely within Lean itself. But a metaprogram is able to make arbitrary system calls with the privileges granted to it. A metaprogram can then identify the VS Code instance associated with its Lean process, open a VS Code debugging interface, and use this interface to control the behavior and appearance of VS Code. The source code for such a metaprogram and a VM configuration are available for inspection. This VM is representative of a standard Ubuntu machine. This demonstration was tested in an Ubuntu 26.04 VM without launching VS Code with special debugging options.

In this demo, the content of Main.lean looks the same as the Sorting.main example above. The user sees double checkmarks, etc. But now, if they dig deeper by opening the Implementation.lean file with Go to Definition, they will see a buffer that is free of metaprogramming. This buffer only contains the implementation of the sorting function.

Unfortunately for the user, the Implementation.lean file imported by Main.lean really does have a metaprogram inside of it. But that metaprogram is designed to hack VS Code and show the user a fake buffer that does not contain the metaprogram. This concealed metaprogram can then use any of the mechanisms discussed thus far. Instead, this metaprogram illustrates an additional attack. It controls VS Code directly to intercept and discard kernel rejection and to draw double checkmarks in the gutter next to the theorems. Running lake env lean Main.lean gives errors in this case. Unlike in the prior demonstrations, the metaprogram here is obscuring the negative response from the kernel inside the interface.

The prior metaprograms exploited the fact that the syntactic form shown to the user need not correspond to the proposition shown to the kernel. The metaprogram in this section illustrates that the user can be misled even if that correspondence is satisfied. Moreover, this metaprogram illustrates that the user experience can be manipulated so thoroughly that metaprograms can hide themselves.

Manipulating the Command Line Directly

On an older version of Ubuntu (22.04), a metaprogram can install aliases in the user's shell after they invoke lake build. The implication is that a user's experience can be manipulated even if they are building and inspecting Lean code using standard command line tools. A metaprogram can modify the behavior of lake clean to persist a malicious Lean object file. Metaprograms can also modify the behavior of cat so that it does not show the true contents of a file. This latter modification can be used to hide a metaprogram from the user. This attack uses a feature that is no longer enabled by default in Ubuntu, so it is unclear whether a similar attack could be conducted inside updated environments. Source code and a VM configuration are available for inspection.