diff --git a/Proof/Attestation.h b/Proof/Attestation.h
new file mode 100644
index 0000000..f78872d
--- /dev/null
+++ b/Proof/Attestation.h
@@ -0,0 +1,214 @@
+/*!
+ * @file
+ * @brief The `Attestation` framework permits code which can provide limited compiletime guarantees of conditions.
+ */
+#pragma once
+
+#include <cassert>
+#include <cstdlib>
+
+#include <utility>
+#include <type_traits>
+
+
+namespace Alepha::Proof
+{
+	template< typename Attestation >
+	Attestation
+	impute()
+	{
+		return Attestation{};
+	}
+
+	template< typename Permission >
+	auto
+	attest( Permission )
+	{	
+		return impute< typename Permission::attestation_type >();
+	}
+
+	#if 0
+	namespace attestation_detail
+	{
+		template< typename ... Args > struct typelist {};
+
+		template< typename T > struct make_typelist;
+
+		template< typename ... Args >
+		struct make_typelist< std::tuple< Args... > >
+		{
+			using type= typelist< Args... >;
+		};
+
+		template< typename Policy, typename = void >
+		struct conjugates
+		{
+			using type= typelist< Policy >;
+		};
+
+		template< typename Policy >
+		struct conjugates< Policy, std::void_t< decltype( typename Policy::conjunction_type{} ) > >
+		{
+			using type= typename make_typelist< typename Policy::conjunction_type >::type;
+		};
+
+
+		template< typename value, typename Conjugates >
+		struct in_set : std::false_type {};
+
+		template< typename value >
+		struct in_set< value, typelist< value > > : std::true_type {};
+
+		template< typename value, typename ... Conjugates >
+		struct in_set< value, typelist< value, Conjugates... > > : std::true_type {};
+
+		template< typename value, typename X, typename ... Conjugates >
+		struct in_set< value, typelist< X, Conjugates... > > : in_set< value, Conjugates... > {};
+
+		template< typename value, typename X >
+		struct in_set< value, typelist< X > > : std::false_type {};
+
+		template< typename A, typename B >
+		struct is_subset_of : std::false_type {};
+
+		template< typename T, typename ... Left, typename ... Right >
+		struct is_subset_of< typelist< T, Left... >, typelist< Right... > >
+				: std::integral_constant< bool, in_set< T, Right... >::value
+						&& is_subset_of< Left..., Right... > > {};
+
+		template< typename ... Right >
+		struct is_subset_of< typelist<>, typelist< Right... > >
+				: std::true_type {};
+
+		template< typename ... Left >
+		struct is_subset_of< typelist< Left... >, typelist<> >
+				: std::false_type {};
+
+		template<>
+		struct is_subset_of< typelist<>, typelist<> > : std::true_type {};
+
+		template< typename ... lists >
+		struct set_union;
+
+		template< typename ... elements >
+		struct set_union< typelist< elements... > > : typelist< elements... > {};
+
+		template< typename ... elements >
+		struct set_union< typelist< elements... > > : typelist< elements... > {};
+	}
+	#endif
+
+	/*!
+	 * @brief An Attestation is a representation of some particular fact about runtime code known at compiletime.
+	 *
+	 * An Attestation is a copyable, zero-storage type which represents at compiletime a fact about runtime code.
+	 * Attestations can be used as compiletime predicates for a function by making that function take an attestation
+	 * as an argument.  Every attestation is created only by the limited set of classes as indicated by the `averant`
+	 * member of the `Policy` for an Attestation.  These policies are also tag types which distinguish the kind of
+	 * Attestation.
+	 *
+	 * Attestations can be copied freely, as any fact once true is considered to continue being true.  Attestations
+	 * should not be held over the long term -- they are best used as temporaries, such as ephemeral arguments to
+	 * a function requiring that fact to be true.
+	 */
+	template< typename Policy >
+	class Attestation
+	{
+		private:
+			struct permission_t { using attestation_type= Attestation; };
+			static inline permission_t permission;
+
+			Attestation()= default;
+
+			template< typename A > friend A impute();
+
+			//template< typename A, typename P > friend A attest( P );
+
+			friend typename Policy::averant;
+
+			//using conjugates= typename attestation_detail::conjugates< Policy >::type;
+
+			template< typename > friend class Attestation;
+
+		public:
+			template< typename > class Witness;
+
+		#if 0
+			template< typename ... Policies >
+			Attestation( Attestation< Policies >... )
+			{
+				static_assert( attestation_detail::is_subset_of< conjugates,
+						typename attestation_detail::set_union< Policies >::type >::value,
+						"Cannot make an attestation without sufficient proof of existance for "
+						"required facts." );
+			}
+
+			template< typename ForeignPolicy >
+			Attestation( Attestation< ForeignPolicy > )
+					//: Attestation( attestation_detail::expand< ForeignPolicy >::
+			{
+				static_assert( attestation_detail::is_subset_of< conjugates,
+						typelist< Attestations... > >::value, "Cannot make an attestation without "
+						"sufficient proof of existance for required facts." );
+			}
+		#endif
+
+			template< typename T >
+			auto 
+			aver( const T &r )
+			{
+				return Witness< const T & >( r );
+			}
+
+			template< typename T >
+			auto 
+			averCopy( T r )
+			{
+				return Witness< T >( std::move( r ) );
+			}
+	};
+
+	/*!
+	 * @brief A witness knows a fact (Attestation) to be true about some particular value.
+	 *
+	 * In the Attestation framework, a Witness is an attestation type which binds a particular fact (a regular Attestation) to the
+	 * value for which that fact is true.  For example, one can create a `Witness` to the fact that a particular `std::vector` is
+	 * sorted.  This is extremely useful as it cuts down on the need to create specialized "constrained" types for specific use cases.
+	 *
+	 * Witnesses are not actually a proxy for the value for which the fact is true.  A witness must `testify` as to which value the
+	 * fact is actually true for.  The `testify` function returns the actual value for which the `Attestation` is known to hold.
+	 */
+	template< typename Policy >
+	template< typename T >
+	class Attestation< Policy >::Witness
+	{
+		private:
+			T value;
+
+			friend Attestation< Policy >;
+
+			explicit Witness( T i_v ) : value( std::move( i_v ) ) {}
+
+		public:
+			inline friend T &testify( Witness &w ) noexcept { return w.value; }
+			inline friend T const &testify( const Witness &w ) noexcept { return w.value; }
+			inline friend Attestation< Policy > fact( Witness w ) noexcept
+					{ return Attestation< Policy >{}; }
+	};
+
+	template< typename Policy >
+	template< typename T >
+	class Attestation< Policy >::Witness< T & >
+	{
+		private:
+			T *p;
+
+			friend Attestation< Policy >;
+
+			explicit Witness( T &r ) : p( &r ) {}
+
+		public:
+			friend T &testify( Witness w ) noexcept { return *w.p; }
+			friend Attestation< Policy > fact( Witness w ) noexcept { return Attestation< Policy >{}; }
+	};
+}
diff --git a/Proof/Makefile b/Proof/Makefile
new file mode 100644
index 0000000..7d99331
--- /dev/null
+++ b/Proof/Makefile
@@ -0,0 +1,12 @@
+#CXX=clang++
+CXX=g++
+CXXFLAGS+= -std=c++1z
+#CXXFLAGS+= -stdlib=libstdc++
+CXXFLAGS+= -O3
+all: simple test
+
+test.cc: Attestation.h
+simple.cc: Attestation.h
+
+clean:
+	$(RM) *.o test
diff --git a/Proof/simple.cc b/Proof/simple.cc
new file mode 100644
index 0000000..91202c0
--- /dev/null
+++ b/Proof/simple.cc
@@ -0,0 +1,134 @@
+#include "Attestation.h"
+#include <iostream>
+#include <iomanip>
+#include <iterator>
+#include <vector>
+#include <algorithm>
+#include <mutex>
+#include <exception>
+
+// Ignore the headers, for the moment, just assume that I have included what I need.
+
+
+namespace
+{
+	// An initial way you might do things...
+	class Thing0
+	{
+		private:
+			std::mutex mtx;
+
+			void helper_needs_lock() {}
+
+
+		public:
+			void
+			function()
+			{
+				std::lock_guard< std::mutex > lock( mtx );
+				helper_needs_lock();
+			}
+	};
+
+
+	// A better way you might do it.
+	class Thing1
+	{
+		private:
+			std::mutex mtx;
+
+			void helper( const std::lock_guard< std::mutex > & ) {}
+
+
+		public:
+			void
+			function()
+			{
+				std::lock_guard< std::mutex > lock( mtx );
+				helper( lock );
+			}
+	};
+
+
+
+	// A more adaptable way you might do it.
+	class WithLock
+	{
+		public:
+			WithLock( const std::lock_guard< std::mutex > & ) {}
+			WithLock( const std::unique_lock< std::mutex > &lock ) { assert( lock.owns_lock() ); }
+	};
+
+	class Thing2
+	{
+		private:
+			std::mutex mtx;
+
+			void helper( WithLock ) {}
+
+
+		public:
+			void
+			function()
+			{
+				std::lock_guard< std::mutex > lock( mtx );
+				helper( lock );
+			}
+	};
+
+
+
+
+
+
+
+
+	// How might we generalize this?
+
+
+
+
+
+	struct Sorter;
+	struct sorted_tag { using averant= Sorter; };
+
+	using Sorted= Alepha::Proof::Attestation< sorted_tag >;
+
+	struct Sorter
+	{
+		static Sorted::Witness< const std::vector< int > & >
+		sort( std::vector< int > &v )
+		{
+			std::sort( begin( v ), end( v ) );
+			return attest( Sorted::permission ).aver< const std::vector< int > & >( v );
+		}
+
+		static Sorted::Witness< const std::vector< int > & >
+		check( std::vector< int > &v )
+		{
+			if( !std::is_sorted( begin( v ), end( v ) ) ) throw std::runtime_error( "" );
+			return attest( Sorted::permission ).aver< const std::vector< int > & >( v );
+		}
+	};
+}
+
+namespace // Other guy
+{
+	bool
+	binarySearch( Sorted::Witness< const std::vector< int > & > v, const int data )
+	{
+		return std::binary_search( begin( testify( v ) ), end( testify( v ) ), data );
+	}
+}
+
+
+int
+main()
+{
+	auto data= std::vector< int >( std::istream_iterator< int >( std::cin ),
+			std::istream_iterator< int >() );
+	auto witness= Sorter::check( data );
+
+	std::cout << std::boolalpha << binarySearch( witness, 42 ) << std::endl;
+}
+
diff --git a/Proof/test.cc b/Proof/test.cc
new file mode 100644
index 0000000..caf6cfc
--- /dev/null
+++ b/Proof/test.cc
@@ -0,0 +1,187 @@
+#include "Attestation.h"
+
+#include <cstddef>
+#include <cstdlib>
+#include <algorithm>
+#include <vector>
+#include <mutex>
+#include <memory>
+
+#include <random>
+
+namespace
+{
+	struct Tester;
+	struct foobar_tag { using averant= Tester; };
+
+	using FoobarFact= Alepha::Proof::Attestation< foobar_tag >;
+
+	struct Tester
+	{
+		static void
+		test()
+		{
+			FoobarFact token= Alepha::Proof::impute< FoobarFact >();
+			FoobarFact token2= attest( FoobarFact::permission );
+		}
+	};
+
+	struct Sorter;
+	struct sorted_tag { using averant= Sorter; };
+
+	using Sorted= Alepha::Proof::Attestation< sorted_tag >;
+
+	struct Sorter
+	{
+		static Sorted::Witness< const std::vector< int > & >
+		sort( std::vector< int > &v )
+		{
+			std::sort( begin( v ), end( v ) );
+			return attest( Sorted::permission ).aver< const std::vector< int > & >( v );
+		}
+	};
+
+	struct Locker;
+	struct with_lock_tag { using averant= Locker; };
+
+	using Locked= Alepha::Proof::Attestation< with_lock_tag >;
+
+	struct Locker
+	{
+		struct WithLock : Locked
+		{
+			public:
+				WithLock( const std::lock_guard< std::mutex > & )
+						: Locked( attest( Locked::permission ) ) {}
+
+				WithLock( std::lock_guard< std::mutex > && )= delete;
+		};
+	};
+
+	using WithLock= Locker::WithLock;
+
+	struct NullChecker;
+	struct non_null_tag { using averant= NullChecker; };
+
+	using NonNull= Alepha::Proof::Attestation< non_null_tag >;
+
+	struct NullChecker
+	{
+		template< typename Ptype >
+		static NonNull::Witness< Ptype >
+		isNotNull( Ptype p )
+		{
+			if( !p ) throw std::logic_error( "" );
+			return attest( NonNull::permission ).averCopy( std::move( p ) );
+		}
+	};
+
+	template< typename P >
+	auto
+	makeUnique()
+	{
+		return NullChecker::isNotNull( std::make_unique< P >() );
+	}
+
+	// Page aligned example
+
+	struct page_aligned_tag { using averant= struct AlignmentChecker; };
+	using PageAligned= Alepha::Proof::Attestation< page_aligned_tag >;
+
+	struct AlignmentChecker
+	{
+		template< typename Ptype >
+		static auto
+		check( Ptype *pointer )
+		{
+			if( pointer % 4096 ) throw std::runtime_error( "" );
+			return attest( PageAligned::permission ).template averCopy< Ptype *const >( pointer );
+		}
+
+		static PageAligned::Witness< void *const >
+		allocate( const std::size_t amt )
+		{
+			void *rv;
+			const int ec= posix_memalign( &rv, 4096, amt );
+			if( ec ) std::get_new_handler()();
+			return attest( PageAligned::permission ).averCopy< void *const >( rv );
+		}
+	};
+
+
+	template< typename T >
+	PageAligned::Witness< std::unique_ptr< T > >
+	make_unique_on_page()
+	{
+		// Dtor ordering and transition of responsibility struct
+		struct Safety
+		{
+			std::unique_ptr< void > memory;
+
+			explicit Safety( void *p ) : memory( p ) { new (p) T(); }
+
+			~Safety()= delete;
+
+			std::unique_ptr< T >
+			finish () & noexcept
+			{
+				return std::unique_ptr< T >( reinterpret_cast< T * >( memory.release() ) );
+			}
+		};
+
+		auto safe_adapt= []( auto p )
+		{
+			std::array< std::uint8_t, sizeof( Safety ) > locals;
+			auto safe= (new (locals.data()) Safety( witness( p ) ))->finish();
+			return std::make_pair( std::move( safe ), fact( p ) );
+		};
+
+		auto [ ptr, alignment ]= safe_adapt( AlignmentChecker::allocate( sizeof( T ) ) );
+
+		return alignment.template averCopy< std::unique_ptr< T > >( std::move( ptr ) );
+	}
+}
+
+
+int
+main()
+{
+	Tester::test();
+	//attest( FoobarFact::permission );
+	FoobarFact token= Alepha::Proof::impute< FoobarFact >();
+
+	std::vector< int > v{ 5, 11, 3, 2, 1 };
+	Sorted::Witness< const std::vector< int > & > sortedVector= Sorter::sort( v );
+	assert( std::is_sorted( begin( testify( sortedVector ) ), end( testify( sortedVector ) ) ) );
+
+	std::shuffle( begin( v ), end( v ), std::random_device() );
+
+	assert( !std::is_sorted( begin( testify( sortedVector ) ), end( testify( sortedVector ) ) ) );
+
+
+	std::mutex mtx;
+
+	auto checker= []( WithLock ) {};
+
+	std::lock_guard< std::mutex > lk( mtx );
+	checker( lk );
+
+	auto myInt= makeUnique< int >();
+	return EXIT_SUCCESS;
+}
+
+
+
+namespace
+{
+	namespace mongo
+	{
+		struct OperationContext { int member; };
+		void
+		operation( NonNull::Witness< OperationContext * > opCtx )
+		{
+			// ...
+			(void) testify( opCtx )->member;
+		}
+	}
+}