Automated Theorem Proving on seL4
77.6Proof Success RateStepwise (Mistral)
Evaluation results
| Method | Links | |
|---|---|---|
| Stepwise (Mistral)Category=Ours, Backbone=Mistral-7B2026.03 | 77.6 | |
| Stepwise (Qwen3)Category=Ours, Backbone=Qwen3-1.7B2026.03 | 70.4 | |
| SledgehammerCategory=Symbolic2026.03 | 40.3 | |
| FVELCategory=Neural, Model=Mistral 7B-Instruct2026.03 | 7.8 | |
| AutoCategory=Symbolic2026.03 | 5.9 | |
| SeleneCategory=Neural, Model=GPT-4o2026.03 | 5.6 |