Add kmir tool description and CI workflow - #310

Merged

feliperodri merged 62 commits into

model-checking:mainfrom

runtimeverification:add-kmir-tool

Aug 21, 2026

Commits on Apr 1, 2025

add KMIR to the docs using prepared tool template text
jberthold
committed
14ee0f2
add kmir workflow and proof claim files + source. WIP README.mds need adjustments
jberthold
committed
39bbca7
remove stray quotes
jberthold
committed
4082f8a
New README.md for the KMIR proof top directory
jberthold
committed
572425b
Adjust README for maximum-example-proof
jberthold
committed
ca8f7e7
adjust steps in maximum proof, give an example of the configuration
jberthold
committed
822f8ec
use demon container in workflow
jberthold
committed
8d9de92

Commits on Apr 2, 2025

Commits on Apr 4, 2025

Merge branch 'main' into add-kmir-tool
jberthold
authored
fc9eecf

Commits on Apr 5, 2025

Format Markdown files to 80-column line breaks (content unchanged)
jberthold
committed
5746c4d
Edits round 1, see related issue
jberthold
committed
3acce27

Commits on Apr 6, 2025

Commits on Apr 7, 2025

Commits on Apr 9, 2025

Merge branch 'main' into add-kmir-tool
jberthold
authored
f73b9a2

Commits on Apr 15, 2025

Commits on Apr 18, 2025

Update kmir.md
gregorymakodzeba
authored
7b857e9

Commits on Apr 28, 2025

Update kmir-proofs/maximum-example-proof/README.md

dkcumming
and
tautschnig
authored
bc50f5a

Commits on May 6, 2025

Merge branch 'main' into add-kmir-tool
jberthold
authored
8f2a189

Commits on May 15, 2025

Merge branch 'main' into add-kmir-tool
jberthold
authored
73aadd0

Commits on Apr 16, 2026

Rename Stable MIR to Public MIR
dkcumming
committed
76f49d7
Updated installation and usage sections
dkcumming
committed
e4377e7
Added section on useful proving flags
dkcumming
committed
a0ca60d
s/symbollic/symbolic & s/Solitidy/Solidity
dkcumming
committed
e58fcdb
Added installation gif
dkcumming
committed
e095f63

Commits on Apr 17, 2026

Added passing proof and show gif
dkcumming
committed
35ac703
Added failing proof with view gif
dkcumming
committed
e5722ec
Added some examples and clarity for loops.
dkcumming
committed
39a45e2
Added section on KMIR proof harnesses
dkcumming
committed
8632482
Added case study for Challenge 11
dkcumming
committed
961ff61
Added case study for P-Token proofs
dkcumming
committed
7694bc8
Added known limitations sections
dkcumming
committed
c2953b4
Use `ubuntu-jammy-latest` as docker release in workflow
dkcumming
committed
d7f7537

Commits on Apr 18, 2026

Added challenge 11 proofs to workflow
dkcumming
committed
659f410

Commits on Apr 21, 2026

Updated `run-proofs.sh` to reuse `llvm-kompile`
dkcumming
committed
be2c7e9
Added parallel execution of 2 for run-proofs.sh
dkcumming
committed
9e5dd9d
Merge remote-tracking branch 'upstream/main' into add-kmir-tool
dkcumming
committed
02c1126

Commits on Apr 23, 2026

Commits on Jul 20, 2026

Merge branch 'main' into add-kmir-tool
dkcumming
authored
c597479

Commits on Aug 20, 2026