# Exploit Test Files

**Note**: Each tool is designed for different purposes and performing according to its specifications.

## Tool Comparison Results

| Exploit | LeanParanoia | lean4checker | SafeVerify | Comparator |
|---------|--------------|--------------|------------|------------|
| AuxiliaryShadowing/MatcherShadowing [↗](tests/lean_exploit_files/AuxiliaryShadowing/MatcherShadowing.lean) | 🟢 1460ms (1488ms) | 🟢 2313ms | <details><summary>🛑 1480ms</summary>definition LeanTestProject.AuxiliaryShadowing.MatcherShadowing.foo does not match the requirement</details> | <details><summary>🟡 2843ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| AuxiliaryShadowing/PrivateShadowing [↗](tests/lean_exploit_files/AuxiliaryShadowing/PrivateShadowing.lean) | 🟢 1463ms (1445ms) | 🟢 2304ms | <details><summary>🛑 1499ms</summary>definition LeanTestProject.AuxiliaryShadowing.PrivateShadowing.foo does not match the requirement</details> | <details><summary>🟡 2907ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| AuxiliaryShadowing/ProofShadowing [↗](tests/lean_exploit_files/AuxiliaryShadowing/ProofShadowing.lean) | 🟢 1587ms (1538ms) | 🟢 2444ms | <details><summary>🛑 1575ms</summary>definition LeanTestProject.AuxiliaryShadowing.ProofShadowing.foo does not match the requirement</details> | <details><summary>🟡 3193ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| AuxiliaryShadowing/TheoremShadowing [↗](tests/lean_exploit_files/AuxiliaryShadowing/TheoremShadowing.lean) | <details><summary>🛑 1650ms (1580ms)</summary>Replay</details> | 🟢 2382ms | <details><summary>🛑 1604ms</summary>theorem LeanTestProject.AuxiliaryShadowing.TheoremShadowing.exploit does not have the same type as the requirement</details> | <details><summary>🟡 3216ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| AuxiliaryShadowing/TypeSignature [↗](tests/lean_exploit_files/AuxiliaryShadowing/TypeSignature.lean) | <details><summary>🛑 1616ms (1680ms)</summary>Replay</details> | 🟢 2446ms | <details><summary>🛑 1532ms</summary>definition LeanTestProject.AuxiliaryShadowing.TypeSignature.exploit does not match the requirement</details> | <details><summary>🟡 3204ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| CSimp/WithAxiom [↗](tests/lean_exploit_files/CSimp/WithAxiom.lean) | <details><summary>🛑 1652ms (1096ms)</summary>CSimp; CustomAxioms</details> | 🟢 2527ms | <details><summary>🛑 1572ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4532ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| CSimp/WithUnsafe [↗](tests/lean_exploit_files/CSimp/WithUnsafe.lean) | <details><summary>🛑 1722ms (1114ms)</summary>CSimp; CustomAxioms</details> | 🟢 2483ms | <details><summary>🛑 1619ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4483ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| ConstructorIntegrity/ManualConstructor [↗](tests/lean_exploit_files/ConstructorIntegrity/ManualConstructor.lean) | <details><summary>🛑 1511ms (1049ms)</summary>ConstructorIntegrity; CustomAxioms; RecursorIntegrity</details> | 🟢 2471ms | <details><summary>🛑 1687ms</summary>definition exploit_theorem does not match the requirement</details> | <details><summary>🛑 4360ms</summary>Challenge and solution constant kind don't match: 'exploit_theorem'</details> |
| CustomAxioms/FakeStdLib [↗](tests/lean_exploit_files/CustomAxioms/FakeStdLib.lean) | <details><summary>🛑 3765ms (1552ms)</summary>CustomAxioms</details> | 🟢 2908ms | <details><summary>🛑 2035ms</summary>Std.TrustMe.forgedFalse is not in the allowed set of standard axioms</details> | <details><summary>🛑 4879ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| CustomAxioms/ForgeRunCmd [↗](tests/lean_exploit_files/CustomAxioms/ForgeRunCmd.lean) | <details><summary>🛑 3725ms (1549ms)</summary>CustomAxioms</details> | 🟢 3067ms | <details><summary>🛑 2087ms</summary>RunCmdForgedFalse is not in the allowed set of standard axioms</details> | <details><summary>🛑 4962ms</summary>Challenge and solution constant kind don't match: 'exploit_theorem'</details> |
| CustomAxioms/ForgeRunTac [↗](tests/lean_exploit_files/CustomAxioms/ForgeRunTac.lean) | <details><summary>🛑 3855ms (1487ms)</summary>CustomAxioms</details> | 🟢 2840ms | <details><summary>🛑 2105ms</summary>RunTacForgedFalse is not in the allowed set of standard axioms</details> | <details><summary>🛑 5002ms</summary>Challenge and solution constant kind don't match: 'exploit_theorem'</details> |
| CustomAxioms/HiddenInInstance [↗](tests/lean_exploit_files/CustomAxioms/HiddenInInstance.lean) | <details><summary>🛑 1652ms (1072ms)</summary>CustomAxioms</details> | 🟢 2443ms | <details><summary>🛑 1527ms</summary>LeanTestProject.CustomAxioms.HiddenInInstance.hidden_axiom is not in the allowed set of standard axioms</details> | <details><summary>🟡 3068ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| CustomAxioms/HiddenInMacro [↗](tests/lean_exploit_files/CustomAxioms/HiddenInMacro.lean) | <details><summary>🛑 1604ms (999ms)</summary>CustomAxioms</details> | 🟢 2352ms | <details><summary>🛑 1530ms</summary>LeanTestProject.CustomAxioms.HiddenInMacro.hidden_axiom is not in the allowed set of standard axioms</details> | <details><summary>🟡 2968ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| CustomAxioms/ProveAnything [↗](tests/lean_exploit_files/CustomAxioms/ProveAnything.lean) | <details><summary>🛑 1559ms (985ms)</summary>CustomAxioms</details> | 🟢 2449ms | <details><summary>🛑 1532ms</summary>magic is not in the allowed set of standard axioms</details> | <details><summary>🛑 4061ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| CustomAxioms/ProveFalse [↗](tests/lean_exploit_files/CustomAxioms/ProveFalse.lean) | <details><summary>🛑 1499ms (940ms)</summary>CustomAxioms</details> | 🟢 2355ms | <details><summary>🛑 1550ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4414ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| CustomAxioms/SkipKernelTC [↗](tests/lean_exploit_files/CustomAxioms/SkipKernelTC.lean) | <details><summary>🛑 1625ms (1052ms)</summary>CustomAxioms</details> | 🟢 2459ms | 🟢 1651ms | <details><summary>🛑 4347ms</summary>Solution constant is not a theorem: 'exploit_theorem'</details> |
| Extern/BuiltinInit [↗](tests/lean_exploit_files/Extern/BuiltinInit.lean) | <details><summary>🛑 2004ms (1052ms)</summary>CustomAxioms; Extern</details> | 🟢 2486ms | <details><summary>🛑 1636ms</summary>theorem exploit_theorem does not have the same type as the requirement</details> | <details><summary>🛑 4351ms</summary>Challenge and solution theorem statement do not match: 'exploit_theorem'</details> |
| Extern/CoreNamespace [↗](tests/lean_exploit_files/Extern/CoreNamespace.lean) | <details><summary>🛑 1720ms (1102ms)</summary>CustomAxioms; Extern</details> | 🟢 2515ms | <details><summary>🛑 1621ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4389ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Extern/ExportC [↗](tests/lean_exploit_files/Extern/ExportC.lean) | <details><summary>🛑 1679ms (1061ms)</summary>CustomAxioms; Extern</details> | 🟢 2494ms | <details><summary>🛑 1675ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4442ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Extern/ExternFFI [↗](tests/lean_exploit_files/Extern/ExternFFI.lean) | <details><summary>🛑 1619ms (1081ms)</summary>CustomAxioms; Extern</details> | 🟢 2515ms | <details><summary>🛑 1753ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4345ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Extern/InitHook [↗](tests/lean_exploit_files/Extern/InitHook.lean) | <details><summary>🛑 2064ms (1105ms)</summary>CustomAxioms; Extern</details> | 🟢 2557ms | <details><summary>🛑 1563ms</summary>theorem exploit_theorem does not have the same type as the requirement</details> | <details><summary>🛑 4436ms</summary>Challenge and solution theorem statement do not match: 'exploit_theorem'</details> |
| Extern/PrivateExtern [↗](tests/lean_exploit_files/Extern/PrivateExtern.lean) | <details><summary>🛑 1583ms (1053ms)</summary>CustomAxioms; Extern</details> | 🟢 2357ms | <details><summary>🛑 1654ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4482ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| ImplementedBy/ChainedReplacement [↗](tests/lean_exploit_files/ImplementedBy/ChainedReplacement.lean) | <details><summary>🛑 1707ms (1072ms)</summary>CustomAxioms; Extern; ImplementedBy</details> | 🟢 2505ms | <details><summary>🛑 1673ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4660ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| ImplementedBy/DirectReplacement [↗](tests/lean_exploit_files/ImplementedBy/DirectReplacement.lean) | <details><summary>🛑 1710ms (1099ms)</summary>CustomAxioms; ImplementedBy; Unsafe</details> | 🟢 2567ms | <details><summary>🛑 1660ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4418ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| ImplementedBy/PrivateImpl [↗](tests/lean_exploit_files/ImplementedBy/PrivateImpl.lean) | <details><summary>🛑 1678ms (1110ms)</summary>CustomAxioms; ImplementedBy; Unsafe</details> | 🟢 2459ms | <details><summary>🛑 1485ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4390ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| KernelRejection/NonPositive [↗](tests/lean_exploit_files/KernelRejection/NonPositive.lean) | <details><summary>🛑 918ms (943ms)</summary>KernelRejection</details> | <details><summary>🛑 2367ms</summary>Could not find any oleans for: LeanTestProject.KernelRejection.NonPositive</details> | <details><summary>🟡 N/A</summary>Kernel rejected during compilation</details> | <details><summary>🛑 3015ms</summary>Child exited with 1</details> |
| KernelRejection/UnsafeCast [↗](tests/lean_exploit_files/KernelRejection/UnsafeCast.lean) | <details><summary>🛑 893ms (915ms)</summary>KernelRejection</details> | <details><summary>🛑 2279ms</summary>Could not find any oleans for: LeanTestProject.KernelRejection.UnsafeCast</details> | <details><summary>🟡 N/A</summary>Kernel rejected during compilation</details> | <details><summary>🛑 3031ms</summary>Child exited with 1</details> |
| Metavariables/Timeout [↗](tests/lean_exploit_files/Metavariables/Timeout.lean) | <details><summary>🛑 1583ms (1104ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2536ms | <details><summary>🛑 1646ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4515ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Metavariables/TypeclassFail [↗](tests/lean_exploit_files/Metavariables/TypeclassFail.lean) | <details><summary>🛑 1669ms (1109ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2516ms | <details><summary>🛑 1642ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4478ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| NativeComputation/NativeDecide [↗](tests/lean_exploit_files/NativeComputation/NativeDecide.lean) | <details><summary>🛑 1821ms (1081ms)</summary>CustomAxioms; NativeComputation; Replay</details> | <details><summary>🛑 2514ms</summary>(kernel) (interpreter) unknown declaration 'exploit_theorem._nativeDecide_1_1'</details> | <details><summary>🛑 1670ms</summary>(kernel) (interpreter) unknown declaration 'exploit_theorem._nativeDecide_1_1'</details> | <details><summary>🛑 4454ms</summary>Challenge and solution theorem statement do not match: 'exploit_theorem'</details> |
| NativeComputation/OfReduce [↗](tests/lean_exploit_files/NativeComputation/OfReduce.lean) | <details><summary>🛑 2180ms (1212ms)</summary>CustomAxioms; NativeComputation; Replay</details> | <details><summary>🛑 2598ms</summary>(kernel) (interpreter) unknown declaration 'exploit_theorem._nativeDecide_1_1'</details> | <details><summary>🛑 1654ms</summary>(kernel) (interpreter) unknown declaration 'exploit_theorem._nativeDecide_1_1'</details> | <details><summary>🛑 4069ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Partial/NonTerminating [↗](tests/lean_exploit_files/Partial/NonTerminating.lean) | <details><summary>🛑 1569ms (938ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2334ms | <details><summary>🛑 1503ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🟡 3137ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| RecursorIntegrity/MissingRecursor [↗](tests/lean_exploit_files/RecursorIntegrity/MissingRecursor.lean) | <details><summary>🛑 1573ms (1032ms)</summary>ConstructorIntegrity; CustomAxioms; RecursorIntegrity</details> | 🟢 2479ms | <details><summary>🛑 1586ms</summary>definition exploit_theorem does not match the requirement</details> | <details><summary>🛑 4047ms</summary>Challenge and solution constant kind don't match: 'exploit_theorem'</details> |
| Sorry/Admit [↗](tests/lean_exploit_files/Sorry/Admit.lean) | <details><summary>🛑 1492ms (1013ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2423ms | <details><summary>🛑 1647ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4434ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Sorry/ByAsSorry [↗](tests/lean_exploit_files/Sorry/ByAsSorry.lean) | <details><summary>🛑 1630ms (1043ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2434ms | <details><summary>🛑 1677ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4199ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Sorry/Direct [↗](tests/lean_exploit_files/Sorry/Direct.lean) | <details><summary>🛑 1545ms (935ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2289ms | <details><summary>🛑 1472ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🟡 3087ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| Sorry/Intermediate [↗](tests/lean_exploit_files/Sorry/Intermediate.lean) | <details><summary>🛑 1711ms (1083ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2499ms | <details><summary>🛑 1743ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4925ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Sorry/Opaque [↗](tests/lean_exploit_files/Sorry/Opaque.lean) | <details><summary>🛑 4574ms (1725ms)</summary>CustomAxioms; Sorry</details> | 🟢 3100ms | <details><summary>🛑 2037ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4506ms</summary>Challenge and solution constant kind don't match: 'exploit_theorem'</details> |
| Sorry/ProofAsSorry [↗](tests/lean_exploit_files/Sorry/ProofAsSorry.lean) | <details><summary>🛑 1551ms (1082ms)</summary>CustomAxioms; Sorry</details> | 🟢 2537ms | <details><summary>🛑 1698ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4483ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Sorry/TerminalTactics [↗](tests/lean_exploit_files/Sorry/TerminalTactics.lean) | <details><summary>🛑 1687ms (1052ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2430ms | <details><summary>🛑 1605ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4367ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Sorry/Underscore [↗](tests/lean_exploit_files/Sorry/Underscore.lean) | <details><summary>🛑 1672ms (1116ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2456ms | <details><summary>🛑 1692ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4457ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| SourcePatterns/LocalInstance [↗](tests/lean_exploit_files/SourcePatterns/LocalInstance.lean) | <details><summary>🛑 1553ms (998ms)</summary>SourcePatterns</details> | 🟢 2331ms | <details><summary>🛑 1478ms</summary>theorem LeanTestProject.SourcePatterns.LocalInstance.exploit_theorem does not have the same type as the requirement</details> | <details><summary>🟡 2948ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| SourcePatterns/LocalInstanceArithmetic [↗](tests/lean_exploit_files/SourcePatterns/LocalInstanceArithmetic.lean) | <details><summary>🛑 1628ms (1060ms)</summary>SourcePatterns</details> | 🟢 2472ms | <details><summary>🛑 1639ms</summary>theorem exploit_theorem does not have the same type as the requirement</details> | <details><summary>🛑 4371ms</summary>Challenge and solution theorem statement do not match: 'exploit_theorem'</details> |
| SourcePatterns/LocalMacroRules [↗](tests/lean_exploit_files/SourcePatterns/LocalMacroRules.lean) | <details><summary>🛑 1627ms (1052ms)</summary>CustomAxioms; SourcePatterns</details> | 🟢 2412ms | <details><summary>🛑 1601ms</summary>LeanTestProject.SourcePatterns.LocalMacroRules.hidden_axiom is not in the allowed set of standard axioms</details> | <details><summary>🟡 3165ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| SourcePatterns/LocalNotation [↗](tests/lean_exploit_files/SourcePatterns/LocalNotation.lean) | <details><summary>🛑 1676ms (1074ms)</summary>SourcePatterns</details> | 🟢 2532ms | <details><summary>🛑 1680ms</summary>LeanTestProject.SourcePatterns.LocalNotation.«term_≈_» not found in submission</details> | <details><summary>🟡 3232ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| SourcePatterns/NotationRedefinition [↗](tests/lean_exploit_files/SourcePatterns/NotationRedefinition.lean) | <details><summary>🛑 1682ms (1026ms)</summary>CustomAxioms; SourcePatterns</details> | 🟢 2425ms | <details><summary>🛑 1628ms</summary>theorem LeanTestProject.SourcePatterns.NotationRedefinition.exploit_theorem does not have the same type as the requirement</details> | <details><summary>🟡 3292ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| SourcePatterns/ScopedNotation [↗](tests/lean_exploit_files/SourcePatterns/ScopedNotation.lean) | <details><summary>🛑 1723ms (1101ms)</summary>CustomAxioms; SourcePatterns</details> | 🟢 2508ms | <details><summary>🛑 1689ms</summary>LeanTestProject.SourcePatterns.ScopedNotation._aux_SourcePatterns_ScopedNotation___unexpand_False_1 not found in submission</details> | <details><summary>🟡 3208ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| Transitive/DeepAxiom_L1 [↗](tests/lean_exploit_files/Transitive/DeepAxiom_L1.lean) | <details><summary>🛑 2132ms (1106ms)</summary>CustomAxioms</details> | 🟢 2536ms | <details><summary>🛑 1627ms</summary>custom_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4022ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Transitive/DeepSorry_L1 [↗](tests/lean_exploit_files/Transitive/DeepSorry_L1.lean) | <details><summary>🛑 2016ms (1018ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2455ms | <details><summary>🛑 1632ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4243ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Transitive/DeepSorry_L2 [↗](tests/lean_exploit_files/Transitive/DeepSorry_L2.lean) | <details><summary>🛑 2448ms (1081ms)</summary>CustomAxioms; Sorry; Unsafe</details> | 🟢 2501ms | <details><summary>🛑 1644ms</summary>sorryAx is not in the allowed set of standard axioms</details> | <details><summary>🛑 4491ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Transitive/Level2_UsesBoth [↗](tests/lean_exploit_files/Transitive/Level2_UsesBoth.lean) | 🟢 2129ms (2095ms) | 🟢 2424ms | 🟢 1622ms | <details><summary>🟢 4224ms</summary>Your solution is okay!</details> |
| Transitive/UsesBadLib [↗](tests/lean_exploit_files/Transitive/UsesBadLib.lean) | <details><summary>🛑 1972ms (1016ms)</summary>CustomAxioms</details> | 🟢 2398ms | <details><summary>🛑 1597ms</summary>BadLib.hiddenAssumption is not in the allowed set of standard axioms</details> | <details><summary>🛑 4239ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Unsafe/UnsafeDefinition [↗](tests/lean_exploit_files/Unsafe/UnsafeDefinition.lean) | <details><summary>🛑 1616ms (1102ms)</summary>CustomAxioms; ImplementedBy; Unsafe</details> | 🟢 2473ms | <details><summary>🛑 1648ms</summary>exploit_axiom is not in the allowed set of standard axioms</details> | <details><summary>🛑 4308ms</summary>Illegal axiom detected: 'sorryAx'</details> |
| Valid/ComplexExample [↗](tests/lean_exploit_files/Valid/ComplexExample.lean) | 🟢 1759ms (1702ms) | 🟢 2521ms | <details><summary>🛑 1710ms</summary>_private.Valid.ComplexExample.0.LeanTestProject.Valid.ComplexExample.Tree.size.match_1.eq_1 not found in submission</details> | <details><summary>🟡 2894ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
| Valid/Dependencies [↗](tests/lean_exploit_files/Valid/Dependencies.lean) | 🟢 1911ms (1899ms) | 🟢 2292ms | 🟢 1509ms | <details><summary>🟢 3966ms</summary>Your solution is okay!</details> |
| Valid/Helper [↗](tests/lean_exploit_files/Valid/Helper.lean) | 🟢 1631ms (1554ms) | 🟢 2332ms | 🟢 1541ms | <details><summary>🟢 4254ms</summary>Your solution is okay!</details> |
| Valid/Simple [↗](tests/lean_exploit_files/Valid/Simple.lean) | 🟢 1607ms (1631ms) | 🟢 2477ms | 🟢 1635ms | <details><summary>🟢 4363ms</summary>Your solution is okay!</details> |
| Valid/UnsafeReducibility [↗](tests/lean_exploit_files/Valid/UnsafeReducibility.lean) | 🟢 1627ms (1619ms) | 🟢 2459ms | 🟢 1630ms | <details><summary>🟢 4334ms</summary>Your solution is okay!</details> |
| Valid/WithAxioms [↗](tests/lean_exploit_files/Valid/WithAxioms.lean) | 🟢 1807ms (1821ms) | 🟢 2497ms | 🟢 1663ms | <details><summary>🟡 3247ms</summary>lean4export: PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none</details> |
---

### Legend

- 🛑 **Detected**: Tool identified an exploit
- 🟢 **Passed**: Tool did not detect any exploit
- 🟡 **N/A**: Test setup issue or methodology limitation
- <details><summary>Click to show details</summary>Verification results or tool output</details>


### Timing

- **LeanParanoia**: Verification of pre-compiled `.olean` files (fail-fast time in brackets)
- **Lean4checker**: Kernel re-verification of pre-compiled `.olean` files
- **SafeVerify**: Comparison of pre-compiled `.olean` files
- **Comparator**: Equivalence checking of pre-compiled `.olean` files

Note: WIP, might contain inaccuracies.