Automated Theorem Proving on seL4 (val)
79.8Proof Success RateStepwise (Mistral)
Evaluation results
| Method | Links | |
|---|---|---|
| Stepwise (Mistral)Category=Ours, Backbone=Mistral-7B2026.03 | 79.8 | |
| Stepwise (Qwen3)Category=Ours, Backbone=Qwen3-1.7B2026.03 | 73.6 | |
| SledgehammerCategory=Symbolic2026.03 | 40.5 | |
| FVELCategory=Neural, Model=Mistral 7B-Instruct2026.03 | 8.9 | |
| SeleneCategory=Neural, Model=GPT-4o2026.03 | 6.1 | |
| AutoCategory=Symbolic2026.03 | 4.9 |