diff --git a/sel4-core.md b/sel4-core.md
index e3d0f14..d32855a 100644
--- a/sel4-core.md
+++ b/sel4-core.md
@@ -24,7 +24,7 @@ to build *any* seL4-based system. These include systems built on the
 seL4 Core Platform, but also other classes of systems, such as dynamic
 systems, minimal systems based on directly supporting run-times for
 languages like Rust or Erlang. As such it should not impose policy
-that restricts the design space enabled by se4.
+that restricts the design space enabled by seL4.
 
 This policy freedom applies to both run-time and build-time. 
 
@@ -47,7 +47,7 @@ kernel
 
 #. All the supported boards must support all configurations.
 
-#. The release must include a way test test the functionality and performance of the components.
+#. The release must include a way to test the functionality and performance of the components.
 
 #. All the individual tests and benchmarks must be clearly documented as to their purpose.
 
diff --git a/sel4-platform.md b/sel4-platform.md
index 415bded..590e7d8 100644
--- a/sel4-platform.md
+++ b/sel4-platform.md
@@ -54,7 +54,7 @@ best system for a particular use case, requiring extensive seL4 experience
 from developers.
 
 The seL4 Core Platform addresses this challenge by constraining the
-system architecture and to one that provides enough features and power
+system architecture to one that provides enough features and power
 for this usage class, enabling a much simpler set of developer-visible
 abstractions.
 
@@ -304,7 +304,7 @@ semaphore).
 Memory regions may be attached to a communication channel.
 It is possible for multiple memory regions to be attached to a communication channel.
 
-Attached memory regions provided a way for the PD utilizing the communication channel to refer to a specific memory location.
+Attached memory regions provide a way for the PD utilizing the communication channel to refer to a specific memory location.
 A **memory reference** is an efficient encoding that identifies a specific offset within an attached memory region.
 
 Normally an attached memory region will be mapped into both protection domains, however it is likely that the memory region will be mapped at different virtual address in each PD.
@@ -396,7 +396,7 @@ PPC arguments are passed by-value (i.e. copied) and are limited to 16 machine wo
 > The PPC payload should be considered as analogous to function arguments in the C language; similar limitations exist in the C ABIs (Application Binary Interfaces) of various platforms.
 
 The seL4 Core Platform provides the server with the (non-forgeable)
-identify of the client PD. The server may use this to associate state with the client (e.g. for long-running operations) and enforce
+identity of the client PD. The server may use this to associate state with the client (e.g. for long-running operations) and enforce
 access control.
 
 **Note**