runtimeverification · sukrucildirr · Jun 2, 2025 · Jun 2, 2025 · Jun 2, 2025 · Jun 2, 2025
diff --git a/flake.nix b/flake.nix
@@ -61,7 +61,7 @@
                   "result*"
                   "*.nix"
                   "kevm-pyk/"
-                  # do not include submodule directories that might be initilized empty or non-existent
+                  # do not include submodule directories that might be initialized empty or non-existent
                   "/deps/"
                   "/tests/ethereum-tests"
                   "/web/k-web-theme"
@@ -132,7 +132,7 @@
             projectDir = prev.lib.cleanSource (
               prev.nix-gitignore.gitignoreSourcePure [
                 ./.gitignore
-                # do not include submodule directories that might be initilized empty or non-existent
+                # do not include submodule directories that might be initialized empty or non-existent
                 "/src/kevm_pyk/kproj/plugin"
               ] ./kevm-pyk/.
             );
@@ -210,7 +210,7 @@
               "result*"
               "*.nix"
               "kevm-pyk/"
-              # do not include submodule directories that might be initilized empty or non-existent
+              # do not include submodule directories that might be initialized empty or non-existent
               "/deps/"
               "/tests/ethereum-tests"
               "/web/k-web-theme"

diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -583,7 +583,7 @@ class KEVMSummarizer:
     """
     A class for summarizing the instructions of the KEVM.
 
-    1. `build_spec` builds the proof to symbolically execute one abitrary opcode.
+    1. `build_spec` builds the proof to symbolically execute one arbitrary opcode.
     2. `explore` runs the proof to get the KCFG.
     3. `summarize` minimizes the KCFG to get the summarized rules for opcodes.
     """
@@ -599,7 +599,7 @@ def __init__(self, proof_dir: Path, save_directory: Path) -> None:
         self.save_directory = save_directory
 
     def build_stack_underflow_spec(self) -> APRProof | None:
-        """Build the specification to symbolically execute abitrary instruction with stack underflow."""
+        """Build the specification to symbolically execute arbitrary instruction with stack underflow."""
         ...
 
     def show_proof(

diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -159,7 +159,7 @@ def target_dir(kompiled_targets_dir: Path | None, tmp_path_factory: TempPathFact
 @pytest.fixture(scope='module')
 def kompiled_target_for(target_dir: Path) -> Callable[[Path], Path]:
     """
-    Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec.
+    Generate a function that returns a path to the kompiled definition for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec.
     """
 
     def kompile(spec_file: Path) -> Path:
@@ -263,7 +263,7 @@ def test_kompile_targets(
     """
     This test function is intended to be used to pre-kompile all definitions,
     so that the actual proof tests do not need to do the actual compilation,
-    which is disturbing performance measurment.
+    which is disturbing performance measurement.
 
     To achieve the desired caching, this test should be run like this:
     pytest src/tests/integration/test_prove.py::test_kompile_targets --kompiled-targets-dir ./prekompiled

diff --git a/media/201710-presentation-devcon3.md b/media/201710-presentation-devcon3.md
@@ -444,7 +444,7 @@ head:
    andBool G >=Int 52 *Int I +Int 21
 ```
 
-Verifing ABI compliant contracts
+Verifying ABI compliant contracts
 --------------------------------
 
 . . .

diff --git a/tests/specs/examples/ERC721.sol b/tests/specs/examples/ERC721.sol
@@ -635,7 +635,7 @@ contract ERC721 is Context, ERC165, IERC721, IERC721Metadata {
     /**
      * @dev Base URI for computing {tokenURI}. If set, the resulting URI for each
      * token will be the concatenation of the `baseURI` and the `tokenId`. Empty
-     * by default, can be overriden in child contracts.
+     * by default, can be overridden in child contracts.
      */
     function _baseURI() internal view virtual returns (string memory) {
         return "";

diff --git a/tests/specs/examples/README.md b/tests/specs/examples/README.md
@@ -45,8 +45,8 @@ For `kevm prove`, you can use `kevm show-kcfg ...` or `kevm view-kcfg ...` to ge
   This is the same file that is used for `kevm prove …`.
   - `--save-directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --save-directory save_directory ...`)
   - `--claim claim_label` lets you select an individual claim out of the `spec_file`.
-If the flag is ommited, it’s assumed that only one claim is present.
-If the flag is ommited and more than one claim is present in the `spec_file` then an error will be raised.
+If the flag is omitted, it’s assumed that only one claim is present.
+If the flag is omitted and more than one claim is present in the `spec_file` then an error will be raised.
   - `--spec-module spec_module` is also an inherited option.
 
 The interactive KCFG (`view-kcfg`) puts your terminal in *application mode*.
-Original file line number
+Diff line change
@@ Expand Up / @@ -444,7 +444,7 @@ head: @@
        andBool G >=Int 52 *Int I +Int 21
     ```
-    Verifing ABI compliant contracts
+    Verifying ABI compliant contracts
     --------------------------------
     . . .
@@ Expand Down @@